Commit 6d112dd4 authored by Sylvain Dailler's avatar Sylvain Dailler

fix 862ded13 in case of multiple requires

This takes into account that "introduce" actually split negative
conjunctions.
parent 44ccf071
......@@ -120,10 +120,10 @@ let rec intros kn pr mal expl f =
(* f is going to be removed, preserve its attributes and location in f2 *)
let f2 = t_attr_copy f f2 in
let fl = Split_goal.split_intro_right ?known_map:kn (dequant false f1) in
let idx =
let name = Ident.get_hyp_name ~attrs:f1.t_attrs in
id_fresh (Opt.get_def "H" name) ~attrs:intro_attrs in
let add (subst,dl) f =
let idx =
let name = Ident.get_hyp_name ~attrs:f1.t_attrs in
id_fresh (Opt.get_def "H" name) ~attrs:intro_attrs in
let svs = Mvs.set_diff (t_freevars Mvs.empty f) subst in
let subst, dl = Mvs.fold (fun vs _ (subst,dl) ->
let (subst,_), d = intro_var (subst, []) vs in
......
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