From 0df8820d7fbdd21c46b2b2945b25d770a40de463 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 21 Sep 2003 22:44:27 +0000
Subject: Mise en place d'implicites par noms en v8

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

(limited to 'translate')

diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index ec1405f76a..784c977dd8 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -87,12 +87,12 @@ let pr_sort = function
   | RProp Term.Pos -> str "Set"
   | RType u -> str "Type" ++ pr_opt pr_universe u
 
-let pr_explicitation = function
-  | None -> mt ()
-  | Some n -> str "@" ++ int n ++ str ":="
-
 let pr_expl_args pr (a,expl) =
-  pr_explicitation expl ++ pr (lapp,L) a
+  match expl with
+  | None -> pr (lapp,L) a
+  | Some (_,ExplByPos n) -> str "@" ++ int n ++ str ":=" ++ pr (lapp,L) a
+  | Some (_,ExplByName id) -> 
+      str "(" ++ pr_id id ++ str ":=" ++ pr (lapp,L) a ++ str ")"
 
 let pr_opt_type pr = function
   | CHole _ -> mt ()
-- 
cgit v1.2.3