Commit 4e6335d4 authored by David Hauzar's avatar David Hauzar

Preserving labels of terms representing implication when introducing

premises.
parent 469a6c90
......@@ -23,6 +23,8 @@ open Decl
let rec intros pr f = match f.t_node with
| Tbinop (Timplies,f1,f2) ->
(* split f1 *)
(* f is going to be removed, preserve its labels (and possibly also location) *)
let f2 = t_label_copy f f2 in
let l = Split_goal.split_pos_intro f1 in
List.fold_right
(fun f acc ->
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment