Méthode plus raisonnable pour supprimer l'inefficacité des evars dépendantes de Anonymous

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

1 files changed, 11 insertions, 10 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 1d5df55f3e..b38adda278 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -186,8 +186,8 @@ let make_evar_instance_with_rel env =
       (fun env (id,b,_) l -> (* if b=None then *) mkVar id :: l (*else l*))
       env ~init:[] in
   snd (fold_rel_context
-	 (fun env (_,b,_) (i,l) -> 
-	    (i-1, (*if b=None then *) mkRel i :: l (*else l*)))
+	 (fun env (na,b,_) (i,l) -> 
+	    (i-1, if na=Anonymous then l else mkRel i :: l))
 	 env ~init:(n,vars))
 
 let make_subst env args =
@@ -206,14 +206,15 @@ let push_rel_context_to_named_context env =
   let sign0 = named_context env in
   let (subst,_,sign) =
   Sign.fold_rel_context
-    (fun (na,c,t) (subst,avoid,sign) ->
-       let na = if na = Anonymous then Name(id_of_string"_") else na in
-       let id = next_name_away na avoid in
-       ((mkVar id)::subst,
-        id::avoid,
-	add_named_decl (id,option_app (substl subst) c,
-                        type_app (substl subst) t)
-	  sign))
+    (fun (na,c,t) (subst,avoid,sign as x) ->
+      if na = Anonymous then x
+      else
+        let id = next_name_away na avoid in
+        ((mkVar id)::subst,
+         id::avoid,
+	 add_named_decl (id,option_app (substl subst) c,
+                         type_app (substl subst) t)
+	   sign))
     (rel_context env) ~init:([],ids_of_named_context sign0,sign0)
   in (subst, sign)