diff options
| author | herbelin | 2005-12-26 13:51:24 +0000 |
|---|---|---|
| committer | herbelin | 2005-12-26 13:51:24 +0000 |
| commit | e0f9487be5ce770117a9c9c815af8c7010ff357b (patch) | |
| tree | bbbde42b0a40803a0c5f5bdb5aaf09248d9aedc0 /proofs | |
| parent | 98d60ce261e7252379ced07d2934647c77efebfd (diff) | |
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacexpr.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 3eccf3d34f..b8de1e789a 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -56,8 +56,7 @@ type hyp_location_flag = (* To distinguish body and type of local defs *) | InHypTypeOnly | InHypValueOnly -type 'a raw_hyp_location = - 'a * int list * (hyp_location_flag * hyp_location_flag option ref) +type 'a raw_hyp_location = 'a * int list * hyp_location_flag type 'a induction_arg = | ElimOnConstr of 'a @@ -132,12 +131,12 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = (* | TacInstantiate of int * 'constr * (('id * hyp_location_flag,unit) location) *) (* Derived basic tactics *) - | TacSimpleInduction of (quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref) + | TacSimpleInduction of quantified_hypothesis | TacNewInduction of 'constr induction_arg * 'constr with_bindings option - * (intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref) + * intro_pattern_expr option | TacSimpleDestruct of quantified_hypothesis | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option - * (intro_pattern_expr option * (bool ref * intro_pattern_expr list ref list) list ref) + * intro_pattern_expr option | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis | TacDecomposeAnd of 'constr |