diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-16 13:59:08 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-01-16 13:59:08 +0000 |
| commit | 58529cf2252bf6ae386a45c8587bdc9b3285c1c5 (patch) | |
| tree | 9aa9268793411733760b2c29a0c5b222eff1bb33 /tactics/inv.ml | |
| parent | 57d007e67deafa77387e5f22fa4d4f2bb147294a (diff) | |
Ajout motif d'introduction "?" (IntroAnonymous) pour laisser Coq
choisir un nom; utilisation de IntroAnonymous au lieu de None dans
l'argument "with_names" des tactiques induction, inversion et assert.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7880 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index 9597cfa41..b799c939f 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -377,6 +377,8 @@ let rewrite_equations_gene othin neqns ba gl = let rec get_names allow_conj = function | IntroWildcard -> error "Discarding pattern not allowed for inversion equations" + | IntroAnonymous -> + error "Anonymous pattern not allowed for inversion equations" | IntroOrAndPattern [l] -> if allow_conj then if l = [] then (None,[]) else @@ -519,15 +521,15 @@ open Tacexpr let inv k = inv_gen false k NoDep -let half_inv_tac id = inv SimpleInversion None (NamedHyp id) -let inv_tac id = inv FullInversion None (NamedHyp id) -let inv_clear_tac id = inv FullInversionClear None (NamedHyp id) +let half_inv_tac id = inv SimpleInversion IntroAnonymous (NamedHyp id) +let inv_tac id = inv FullInversion IntroAnonymous (NamedHyp id) +let inv_clear_tac id = inv FullInversionClear IntroAnonymous (NamedHyp id) let dinv k c = inv_gen false k (Dep c) -let half_dinv_tac id = dinv SimpleInversion None None (NamedHyp id) -let dinv_tac id = dinv FullInversion None None (NamedHyp id) -let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id) +let half_dinv_tac id = dinv SimpleInversion None IntroAnonymous (NamedHyp id) +let dinv_tac id = dinv FullInversion None IntroAnonymous (NamedHyp id) +let dinv_clear_tac id = dinv FullInversionClear None IntroAnonymous (NamedHyp id) (* InvIn will bring the specified clauses into the conclusion, and then * perform inversion on the named hypothesis. After, it will intro them |