From 87ab5e4f9a4f93d152df721f97a0bcb6cddef973 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 23 Sep 2003 11:18:41 +0000 Subject: 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 --- interp/constrextern.ml | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) (limited to 'interp') diff --git a/interp/constrextern.ml b/interp/constrextern.ml index b34ae524f2..2eae4a51b9 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -738,7 +738,7 @@ let extern_constr_gen at_top scopt env t = let vars = vars_of_env env in let avoid = if at_top then ids_of_context env else [] in extern (not at_top) (scopt,Symbols.current_scopes()) vars - (Detyping.detype env avoid (names_of_rel_context env) t) + (Detyping.detype (at_top,env) avoid (names_of_rel_context env) t) let extern_constr_in_scope at_top scope env t = extern_constr_gen at_top (Some scope) env t @@ -782,13 +782,11 @@ let rec raw_of_pat tenv env = function | PCase ((Some ind,cs),typopt,tm,bv) -> let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in let k = (snd (lookup_mind_specif (Global.env()) ind)).Declarations.mind_nrealargs in - Detyping.detype_case false - (fun tenv _ -> raw_of_pat tenv) - (fun tenv _ -> raw_of_eqn tenv) - tenv avoid env ind cs typopt k tm bv + Detyping.detype_case false (raw_of_pat tenv env)(raw_of_eqn tenv env) + tenv avoid ind cs typopt k tm bv | PCase _ -> error "Unsupported case-analysis while printing pattern" - | PFix f -> Detyping.detype tenv [] env (mkFix f) - | PCoFix c -> Detyping.detype tenv [] env (mkCoFix c) + | PFix f -> Detyping.detype (false,tenv) [] env (mkFix f) + | PCoFix c -> Detyping.detype (false,tenv) [] env (mkCoFix c) | PSort s -> RSort (loc,s) and raw_of_eqn tenv env constr construct_nargs branch = -- cgit v1.2.3