diff options
| author | herbelin | 2008-04-04 14:55:47 +0000 |
|---|---|---|
| committer | herbelin | 2008-04-04 14:55:47 +0000 |
| commit | 5a4cc30c737f113a7c57d14569137b3e06f5639f (patch) | |
| tree | 2a0114f494382fc30f50ad073eaf6ec5def2daed /contrib/interface | |
| parent | c464aab4c1aedad2ae919eb4776ced4d4d23d62a (diff) | |
Quelques améliorations des intro patterns:
- ajout de -> et <- pour substitution immédiate d'une égalité
(comportement à la subst si variable, à la rewrite in * sinon)
- ajout possibilité d'hypothèses avec paramètres
- correction d'un comportement bizarre de l'utilisation des noms dans
cas "[[|] H]" (cf CHANGES)
Ce serait bien d'avoir quelque chose comme "intros (H as <-) (H' as [ | ])"
pour décider de garder les noms, mais la syntaxe est assez
moche. Peut-être un "intros H: <- H': [ | ]" ?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10753 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/interface')
| -rw-r--r-- | contrib/interface/xlate.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index f442bf75ff..63efd543aa 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -633,6 +633,7 @@ let rec xlate_intro_pattern = | IntroIdentifier c -> CT_coerce_ID_to_INTRO_PATT(xlate_ident c) | IntroAnonymous -> xlate_error "TODO: IntroAnonymous" | IntroFresh _ -> xlate_error "TODO: IntroFresh" + | IntroRewrite _ -> xlate_error "TODO: IntroRewrite" let compute_INV_TYPE = function FullInversionClear -> CT_inv_clear |