From 5a4cc30c737f113a7c57d14569137b3e06f5639f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 4 Apr 2008 14:55:47 +0000
Subject: 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
---
 contrib/interface/xlate.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'contrib/interface')

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
-- 
cgit v1.2.3