diff options
| author | Hugo Herbelin | 2014-05-08 17:40:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-05-08 20:44:29 +0200 |
| commit | f87c3a55b1ad52b63ebd0af0cf9f3fb0e8e86f76 (patch) | |
| tree | 348006f1c5abfed0a69e67f3090e479a5d26b58a /toplevel | |
| parent | 8bbd7ceb554f68f0473f492f45e0f909af15992b (diff) | |
Renaming new_induct -> induction; new_destruct -> destruct.
Diffstat (limited to 'toplevel')
| -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 5129beeab3..de0459089f 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -78,12 +78,12 @@ let sumbool = Coqlib.build_coq_sumbool let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb let induct_on c = - new_induct false + induction false [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))] None (None,None) None let destruct_on_using c id = - new_destruct false + destruct false [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))] None (None,Some (dl,IntroOrAndPattern [ @@ -92,7 +92,7 @@ let destruct_on_using c id = None let destruct_on c = - new_destruct false + destruct false [Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))] None (None,None) None @@ -592,7 +592,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). apply_in false false freshz [Loc.ghost, (andb_prop(), NoBindings)] None; Proofview.Goal.enter begin fun gl -> let fresht = fresh_id (Id.of_string "Z") gl in - (new_destruct false [Tacexpr.ElimOnConstr + (destruct false [Tacexpr.ElimOnConstr (Evd.empty,((mkVar freshz,NoBindings)))] None (None, Some (dl,IntroOrAndPattern [[ |