diff options
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index e798d8755..a17ea69fe 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -536,7 +536,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). *) tclREPEAT ( tclTHENSEQ [ - apply_in false freshz [(andb_prop()),Rawterm.NoBindings] None; + apply_in false false freshz [(Evd.empty,andb_prop()),Rawterm.NoBindings] None; fun gl -> let fresht = fresh_id (!avoid) (id_of_string "Z") gsig in @@ -748,8 +748,8 @@ let compute_dec_tact ind lnamesparrec nparrec = Pfedit.by ( tclTHENSEQ [ intros_using fresh_first_intros; intros_using [freshn;freshm]; - assert_as true (dl,Genarg.IntroIdentifier freshH) ( - mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) + assert_tac (Name freshH) ( + mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|]) ) ]); (*we do this so we don't have to prove the same goal twice *) Pfedit.by ( tclTHEN @@ -795,7 +795,7 @@ let compute_dec_tact ind lnamesparrec nparrec = unfold_constr (Lazy.force Coqlib.coq_not_ref); intro; Equality.subst_all; - assert_as true (dl,Genarg.IntroIdentifier freshH3) + assert_tac (Name freshH3) (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|])) ]); Pfedit.by |