From cc1b83979b9978fb2979ae8cda86daddaa62badb Mon Sep 17 00:00:00 2001
From: barras
Date: Fri, 10 Oct 2003 15:42:22 +0000
Subject: changement nouvelle syntaxe (pt fixes)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrextern.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 7a557f858f..7ec783e033 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -274,6 +274,8 @@ let translate_v7_string = function
   | "simpl_plus_r" -> "plus_simpl_r"
   | "fact_growing" -> "fact_le"
   | "lt_mult_left" -> "lt_mult_S_left"
+  | "exists" -> "exists_between"
+  | "IHexists" -> "IHexists_between"
   (* Lists *)
   | "idempot_rev" -> "involutive_rev"
   | "forall" -> "HereAndFurther"
@@ -310,6 +312,8 @@ let translate_v7_string = function
       (s' = "unicite" or s' = "unicity") ->
       "uniqueness"^(String.sub s 7 (String.length s - 7))
   (* Default *)
+  | s when String.length s > 1 && s.[0]='_' ->
+      String.sub s 1 (String.length s - 1)
   | "_" -> 
       msgerrnl (str 
 	"Warning: '_' is no longer an ident; it has been translated to 'x_'");
-- 
cgit v1.2.3