diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-10 15:42:22 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-10-10 15:42:22 +0000 |
| commit | cc1b83979b9978fb2979ae8cda86daddaa62badb (patch) | |
| tree | a13cc08f374cff641aea74a027cf6b7a85ffeb06 /proofs | |
| parent | db1658f0837918e27885c827cc29392068775fa6 (diff) | |
changement nouvelle syntaxe (pt fixes)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/tacexpr.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 75ebb2d28..c6453f076 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -109,10 +109,10 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacInstantiate of int * 'constr (* Derived basic tactics *) - | TacOldInduction of quantified_hypothesis + | TacSimpleInduction of quantified_hypothesis | TacNewInduction of 'constr induction_arg * 'constr with_bindings option * intro_pattern_expr list list - | TacOldDestruct of quantified_hypothesis + | TacSimpleDestruct of quantified_hypothesis | TacNewDestruct of 'constr induction_arg * 'constr with_bindings option * intro_pattern_expr list list |