From 95d4aef96fb7b490b188afe66e8345428e9706ee Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 6 Sep 2003 19:12:08 +0000
Subject: Paramétrisation vis à vis de existential_key

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

(limited to 'translate')

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index a03207f254..5dd8e31c8d 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -43,7 +43,7 @@ let lcast = 100
 let lapp = 10
 let lproj = 9
 let ltop = (200,E)
-let lsimple = (0,E)
+let lsimple = (9,E)
 
 let prec_less child (parent,assoc) =
   if parent < 0 && child = lprod then true
@@ -477,7 +477,10 @@ let rec pr inherited a =
         str "end"),
       latom
   | CHole _ -> str "_", latom
+(*
   | CEvar (_,n) -> str "?" ++ int n, latom
+*)
+  | CEvar (_,n) -> str (Evd.string_of_existential n), latom
   | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom
   | CSort (_,s) -> pr_sort s, latom
   | CCast (_,a,b) ->
-- 
cgit v1.2.3