diff options
| author | herbelin | 2004-03-02 07:04:56 +0000 |
|---|---|---|
| committer | herbelin | 2004-03-02 07:04:56 +0000 |
| commit | 8a1ddc270137f40cd8bbff20de4f41e284055891 (patch) | |
| tree | d3d41549bcd3cff2bbd0db1fb7824e05851941dd /tactics/inv.ml | |
| parent | 1a29faa00f1e2a6f2d71088a769fe2fbc823244a (diff) | |
Generalisation de la syntaxe de 'with_names' pour accepter 'as id' avec id variable de ltac substituable dans la pratique par un intro_case_pattern dans induction, destruct et inversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5415 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index b9574db237..0810caa82a 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -523,15 +523,15 @@ open Tacexpr let inv k = inv_gen false k NoDep -let half_inv_tac id = inv SimpleInversion [] (NamedHyp id) -let inv_tac id = inv FullInversion [] (NamedHyp id) -let inv_clear_tac id = inv FullInversionClear [] (NamedHyp id) +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 dinv k c = inv_gen false k (Dep c) -let half_dinv_tac id = dinv SimpleInversion None [] (NamedHyp id) -let dinv_tac id = dinv FullInversion None [] (NamedHyp id) -let dinv_clear_tac id = dinv FullInversionClear None [] (NamedHyp id) +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) (* InvIn will bring the specified clauses into the conclusion, and then * perform inversion on the named hypothesis. After, it will intro them |