Changement de l'afficheur pour que les variables liées aient un nom indépendant des globaux quand hors but (on garde l'évitement des globaux en but, pour compatibilité)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4458 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 5 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index bef1e2a23c..db2617da33 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -137,7 +137,7 @@ let tuple_ref dep n =
 
 let trad_binder avoid nenv id = function
   | CC_untyped_binder -> RHole (dummy_loc,BinderType (Name id))
-  | CC_typed_binder ty -> Detyping.detype (Global.env()) avoid nenv ty
+  | CC_typed_binder ty -> Detyping.detype (false,Global.env()) avoid nenv ty
 
 let rec push_vars avoid nenv = function
   | [] -> ([],avoid,nenv)
@@ -209,22 +209,22 @@ let rawconstr_of_prog p =
       	let n = List.length l in
       	let cl = List.map (trad avoid nenv) l in
       	let tuple = tuple_ref dep n in
-	let tyl = List.map (Detyping.detype (Global.env()) avoid nenv) tyl in
+	let tyl = List.map (Detyping.detype (false,Global.env()) avoid nenv) tyl in
       	let args = tyl @ cl in
 	RApp (dummy_loc, RRef (dummy_loc, tuple), args)
 
     | CC_case (ty,b,el) ->
 	let c = trad avoid nenv b in
 	let cl = List.map (trad avoid nenv) el in
-	let ty = Detyping.detype (Global.env()) avoid nenv ty in
+	let ty = Detyping.detype (false,Global.env()) avoid nenv ty in
 	ROrderedCase (dummy_loc, RegularStyle, Some ty, c, Array.of_list cl, ref None)
 
     | CC_expr c -> 
-	Detyping.detype (Global.env()) avoid nenv c
+	Detyping.detype (false,Global.env()) avoid nenv c
 
     | CC_hole c -> 
 	RCast (dummy_loc, RHole (dummy_loc, QuestionMark),
-               Detyping.detype (Global.env()) avoid nenv c)
+               Detyping.detype (false,Global.env()) avoid nenv c)
 
   in
   trad [] empty_names_context p