diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-15 14:26:43 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-02-15 14:43:10 +0100 |
| commit | 15b28f0ae1e31506f3fb153fc6e50bc861717eb9 (patch) | |
| tree | c139ad543105cfea7791aab2831f5623cddb4a5e /toplevel | |
| parent | 1a8c37ca352c95b4cd530efbbf47f0e7671d1fb3 (diff) | |
Moving conversion functions to the new tactic API.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index f0c7a3961..c143243b1 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -580,7 +580,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = Tacticals.New.tclTRY ( Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None) ); - Proofview.V82.tactic (simpl_in_hyp (freshz,Locus.InHyp)); + simpl_in_hyp (freshz,Locus.InHyp); (* repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). *) @@ -724,7 +724,7 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None) ); Equality.inj None false None (mkVar freshz,NoBindings); - intros; (Proofview.V82.tactic simpl_in_concl); + intros; simpl_in_concl; Auto.default_auto; Tacticals.New.tclREPEAT ( Tacticals.New.tclTHENLIST [apply (andb_true_intro()); @@ -901,7 +901,7 @@ let compute_dec_tact ind lnamesparrec nparrec = let freshH3 = fresh_id (Id.of_string "H") gl in Tacticals.New.tclTHENLIST [ simplest_right ; - Proofview.V82.tactic (unfold_constr (Lazy.force Coqlib.coq_not_ref)); + unfold_constr (Lazy.force Coqlib.coq_not_ref); intro; Equality.subst_all (); assert_by (Name freshH3) |