From 89884470155c568b8abcdfd3986845f846c6f91a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 5 Oct 2000 19:21:17 +0000
Subject: Bug affichage des implicites; bug de compatibilité LAMBDA/LAMBDALIST

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@658 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/termast.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/parsing/termast.ml b/parsing/termast.ml
index 239dd9fc1a..91111ada39 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -155,7 +155,7 @@ let explicitize =
 	       else tail)
     (* Tail impl args are always printed even if implicit printing is off *)
     | [] -> List.rev lastimplargs
-  in exprec 0 []
+  in exprec 1 []
 
 let implicit_of_ref = function
   | RConstruct (cstrid,_) -> constructor_implicits_list cstrid
@@ -219,8 +219,9 @@ let rec ast_of_raw = function
   | RBinder (_,bk,na,t,c) ->
       let (n,a) = factorize_binder 1 bk na (ast_of_raw t) c in
       let tag = match bk with
-	  (* LAMBDA et LAMBDALIST se comportent pareil *)
-	| BLambda -> if n=1 then "LAMBDA" else "LAMBDALIST"
+	  (* LAMBDA et LAMBDALIST se comportent pareil ... Non ! *)
+	  (* Pour compatibilité des theories, il faut LAMBDALIST partout *)
+	| BLambda -> (* if n=1 then "LAMBDA" else *) "LAMBDALIST"
 	  (* PROD et PRODLIST doivent être distingués à cause du cas *)
 	  (* non dépendant, pour isoler l'implication; peut-être un *)
 	  (* constructeur ARROW serait-il plus justifié ? *) 
-- 
cgit v1.2.3