From cc1b83979b9978fb2979ae8cda86daddaa62badb Mon Sep 17 00:00:00 2001 From: barras Date: Fri, 10 Oct 2003 15:42:22 +0000 Subject: changement nouvelle syntaxe (pt fixes) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/hiddentac.ml | 6 ++++-- tactics/hiddentac.mli | 4 ++-- tactics/tacinterp.ml | 17 ++++++++++------- tactics/tactics.ml | 20 ++++++++++---------- tactics/tactics.mli | 4 ++-- 5 files changed, 28 insertions(+), 23 deletions(-) (limited to 'tactics') diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 0e8725c6ad..046ae4ed1e 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -50,8 +50,10 @@ let h_instantiate n c = abstract_tactic (TacInstantiate (n,c)) (Evar_refiner.instantiate n c) (* Derived basic tactics *) -let h_old_induction h = abstract_tactic (TacOldInduction h) (old_induct h) -let h_old_destruct h = abstract_tactic (TacOldDestruct h) (old_destruct h) +let h_simple_induction h = + abstract_tactic (TacSimpleInduction h) (simple_induct h) +let h_simple_destruct h = + abstract_tactic (TacSimpleDestruct h) (simple_destruct h) let h_new_induction c e idl = abstract_tactic (TacNewInduction (c,e,idl)) (new_induct c e idl) let h_new_destruct c e idl = diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index dba9908a97..82146c01aa 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -53,8 +53,8 @@ val h_instantiate : int -> constr -> tactic (* Derived basic tactics *) -val h_old_induction : quantified_hypothesis -> tactic -val h_old_destruct : quantified_hypothesis -> tactic +val h_simple_induction : quantified_hypothesis -> tactic +val h_simple_destruct : quantified_hypothesis -> tactic val h_new_induction : constr induction_arg -> constr with_bindings option -> intro_pattern_expr list list -> tactic diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index ccd22cc73e..7f1a0943ab 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -587,12 +587,14 @@ let rec intern_atomic lf ist x = | TacDAuto (n,p) -> TacDAuto (n,p) (* Derived basic tactics *) - | TacOldInduction h -> TacOldInduction (intern_quantified_hypothesis ist h) + | TacSimpleInduction h -> + TacSimpleInduction (intern_quantified_hypothesis ist h) | TacNewInduction (c,cbo,ids) -> TacNewInduction (intern_induction_arg ist c, option_app (intern_constr_with_bindings ist) cbo, List.map (List.map (intern_intro_pattern lf ist)) ids) - | TacOldDestruct h -> TacOldDestruct (intern_quantified_hypothesis ist h) + | TacSimpleDestruct h -> + TacSimpleDestruct (intern_quantified_hypothesis ist h) | TacNewDestruct (c,cbo,ids) -> TacNewDestruct (intern_induction_arg ist c, option_app (intern_constr_with_bindings ist) cbo, @@ -1602,13 +1604,14 @@ and interp_atomic ist gl = function | TacDAuto (n,p) -> Auto.h_dauto (n,p) (* Derived basic tactics *) - | TacOldInduction h -> - h_old_induction (interp_quantified_hypothesis ist gl h) + | TacSimpleInduction h -> + h_simple_induction (interp_quantified_hypothesis ist gl h) | TacNewInduction (c,cbo,ids) -> h_new_induction (interp_induction_arg ist gl c) (option_app (interp_constr_with_bindings ist gl) cbo) (List.map (List.map (interp_intro_pattern ist)) ids) - | TacOldDestruct h -> h_old_destruct (interp_quantified_hypothesis ist gl h) + | TacSimpleDestruct h -> + h_simple_destruct (interp_quantified_hypothesis ist gl h) | TacNewDestruct (c,cbo,ids) -> h_new_destruct (interp_induction_arg ist gl c) (option_app (interp_constr_with_bindings ist gl) cbo) @@ -1831,11 +1834,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacDAuto (n,p) -> TacDAuto (n,p) (* Derived basic tactics *) - | TacOldInduction h as x -> x + | TacSimpleInduction h as x -> x | TacNewInduction (c,cbo,ids) -> TacNewInduction (subst_induction_arg subst c, option_app (subst_raw_with_bindings subst) cbo, ids) - | TacOldDestruct h as x -> x + | TacSimpleDestruct h as x -> x | TacNewDestruct (c,cbo,ids) -> TacNewDestruct (subst_induction_arg subst c, option_app (subst_raw_with_bindings subst) cbo, ids) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4f9ab4ad18..f38be2f24c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1459,24 +1459,24 @@ let raw_induct s = tclTHEN (intros_until_id s) (tclLAST_HYP simplest_elim) let raw_induct_nodep n = tclTHEN (intros_until_n n) (tclLAST_HYP simplest_elim) (* This was Induction in 6.3 (hybrid form) *) -let old_induct_id s = +let simple_induct_id s = tclORELSE (raw_induct s) (induction_from_context true true None s []) -let old_induct_nodep = raw_induct_nodep +let simple_induct_nodep = raw_induct_nodep -let old_induct = function - | NamedHyp id -> old_induct_id id - | AnonHyp n -> old_induct_nodep n +let simple_induct = function + | NamedHyp id -> simple_induct_id id + | AnonHyp n -> simple_induct_nodep n (* Destruction tactics *) -let old_destruct_id s = +let simple_destruct_id s = (tclTHEN (intros_until_id s) (tclLAST_HYP simplest_case)) -let old_destruct_nodep n = +let simple_destruct_nodep n = (tclTHEN (intros_until_n n) (tclLAST_HYP simplest_case)) -let old_destruct = function - | NamedHyp id -> old_destruct_id id - | AnonHyp n -> old_destruct_nodep n +let simple_destruct = function + | NamedHyp id -> simple_destruct_id id + | AnonHyp n -> simple_destruct_nodep n (* * Eliminations giving the type instead of the proof. diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 38c31f0159..1f4c5b35cf 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -172,7 +172,7 @@ val elim : constr with_bindings -> constr with_bindings option -> tacti val general_elim_in : identifier -> constr * constr bindings -> constr * constr bindings -> tactic -val old_induct : quantified_hypothesis -> tactic +val simple_induct : quantified_hypothesis -> tactic val general_elim_in : identifier -> constr * constr bindings -> constr * constr bindings -> tactic @@ -184,7 +184,7 @@ val new_induct : constr induction_arg -> constr with_bindings option -> val general_case_analysis : constr with_bindings -> tactic val simplest_case : constr -> tactic -val old_destruct : quantified_hypothesis -> tactic +val simple_destruct : quantified_hypothesis -> tactic val new_destruct : constr induction_arg -> constr with_bindings option -> intro_pattern_expr list list -> tactic -- cgit v1.2.3