diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 19:12:08 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-09-06 19:12:08 +0000 |
| commit | 95d4aef96fb7b490b188afe66e8345428e9706ee (patch) | |
| tree | 3990c1a6bfce095e941d756df5387b63e86e8353 /translate | |
| parent | ef41c3d1f93e2fa82cbaa97adaa03852e8fcd7b8 (diff) | |
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
Diffstat (limited to 'translate')
| -rw-r--r-- | translate/ppconstrnew.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index a03207f25..5dd8e31c8 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) -> |