diff options
| author | herbelin | 2003-09-23 11:18:41 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-23 11:18:41 +0000 |
| commit | 87ab5e4f9a4f93d152df721f97a0bcb6cddef973 (patch) | |
| tree | 53f9e45dc0a5d10f180af85876f45b3cf27ba266 /contrib | |
| parent | 090b29f754f44882a49961764e63be18f0d356c4 (diff) | |
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
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/correctness/pcic.ml | 10 | ||||
| -rw-r--r-- | contrib/first-order/instances.ml | 2 |
2 files changed, 6 insertions, 6 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 diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml index 1dc72eecb8..423df2f3c7 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/first-order/instances.ml @@ -121,7 +121,7 @@ let mk_open_instance id gl m t= let nid=(fresh_id avoid var_id gl) in (Name nid,None,dummy_constr)::(aux (n-1) (nid::avoid)) in let nt=it_mkLambda_or_LetIn revt (aux m []) in - let rawt=Detyping.detype env [] [] nt in + let rawt=Detyping.detype (false,env) [] [] nt in let rec raux n t= if n=0 then t else match t with |