Correction bug #1041 (double cause : non évitement des noms existants en

cas de création de nom par défaut; utilisation de _ comme nom dans evarutil.ml)
+ test régression bug #1041 + allègement syntaxe tactique evar
+ essai de ne pas faire dépendre les evars des variables anonymes afin
  de résoudre le bug #932


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

6 files changed, 38 insertions, 37 deletions

diff --git a/library/nameops.ml b/library/nameops.ml
index b68c095936..6c5000dfef 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -20,8 +20,6 @@ let pr_name = function
   | Anonymous -> str "_"
   | Name id -> pr_id id
 
-let wildcard = id_of_string "_"
-
 (* Utilities *)
 
 let code_of_0 = Char.code '0'
@@ -163,10 +161,7 @@ let next_name_away_with_default default name l =
     | Name str  -> next_ident_away str l
     | Anonymous -> next_ident_away (id_of_string default) l
 
-let next_name_away name l = 
-  match name with
-    | Name str  -> next_ident_away str l
-    | Anonymous -> id_of_string "_"
+let next_name_away = next_name_away_with_default "H"
 
 let pr_lab l = str (string_of_label l)
 
diff --git a/library/nameops.mli b/library/nameops.mli
index 895513a3c0..336099a2ff 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -14,8 +14,6 @@ open Names
 val pr_id : identifier -> Pp.std_ppcmds
 val pr_name : name -> Pp.std_ppcmds
 
-val wildcard : identifier
-
 val make_ident : string -> int option -> identifier
 val repr_ident : identifier -> string * int option
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 469a266974..53c6199127 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -148,17 +148,6 @@ let new_evar_instance sign evd typ ?(src=(dummy_loc,InternalHole)) instance =
   (evar_declare sign newev typ ~src:src evd,
    mkEvar (newev,Array.of_list instance))
 
-let make_evar_instance_with_rel env =
-  let n = rel_context_length (rel_context env) in
-  let vars = 
-    fold_named_context
-      (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*)))
-	 env ~init:(n,vars))
-
 let make_subst env args =
   snd (fold_named_context
     (fun env (id,b,c) (args,l) ->
@@ -171,24 +160,32 @@ let make_subst env args =
 (* [new_isevar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
 
-let push_rel_context_to_named_context env =
-  let (subst,_,env) =
-  Sign.fold_rel_context
-    (fun (na,c,t) (subst,avoid,env) ->
-       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,
-	push_named (id,option_map (substl subst) c,
-                        type_app (substl subst) t)
-	  env))
-    (rel_context env) ~init:([],ids_of_named_context (named_context env),env)
-  in (subst, (named_context_val env))
+let dummy_var = mkVar (id_of_string "_")
+
+let push_rel_context_to_named_context env typ =
+  (* compute the instance relative to the named context *)
+  let vars = 
+    fold_named_context (fun env (id,b,_) l -> mkVar id :: l) env ~init:[] in
+  (* move the rel context to a named context and extend the instance 
+     with vars of the rel context *)
+  let fv = free_rels typ in
+  let avoid = ids_of_named_context (named_context env) in
+  let n = rel_context_length (rel_context env) in
+  let (subst, _, _, inst, env) =
+    Sign.fold_rel_context
+      (fun (na,c,t) (subst, n, avoid, inst, env) -> match na with
+	| Anonymous when not (Intset.mem n fv) -> 
+	    (dummy_var::subst, n-1, avoid, inst, env)
+	| _ ->
+	    let id = next_name_away na avoid in
+	    ((mkVar id)::subst, n-1, id::avoid, mkRel n::inst,
+	    push_named (id,option_map (substl subst) c,substl subst t) env))
+      (rel_context env) ~init:([], n, avoid, vars, env) in
+  (named_context_val env, substl subst typ, inst)
 
 let new_evar evd env ?(src=(dummy_loc,InternalHole)) typ =
-  let subst,sign = push_rel_context_to_named_context env in
-  let typ' = substl subst typ in
-  let instance = make_evar_instance_with_rel env in
+  let sign,typ',instance = push_rel_context_to_named_context env typ in
+  assert (not (dependent dummy_var typ));
   new_evar_instance sign evd typ' ~src:src instance
 
 (* The same using side-effect *)
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index d3283164b0..5c94399336 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -928,7 +928,7 @@ let next_name_not_occuring avoid_flags name l env_names t =
         (* Normally, an anonymous name is not dependent and will not be *)
         (* taken into account by the function concrete_name; just in case *)
         (* invent a valid name *)
-        id_of_string "H"
+        next (id_of_string "H")
 
 (* On reduit une serie d'eta-redex de tete ou rien du tout  *)
 (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *)
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 52fa2a8607..cb67bb2ae5 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -285,7 +285,7 @@ open Evar_tactics
 (* evar creation *)
 
 TACTIC EXTEND evar
-  [ "evar" "(" ident(id) ":" constr(typ) ")" ] -> [ let_evar (Name id) typ ]
+  [ "evar" "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
 | [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
 END
 
diff --git a/test-suite/success/instantiate.v b/test-suite/success/instantiate.v
new file mode 100644
index 0000000000..4224405d90
--- /dev/null
+++ b/test-suite/success/instantiate.v
@@ -0,0 +1,11 @@
+(* Test régression bug #1041 *)
+
+Goal Prop.
+
+pose (P:= fun x y :Prop => y).
+evar (Q: forall X Y,P X Y -> Prop) .
+
+instantiate (1:= fun _ => _ ) in (Value of Q).
+instantiate (1:= fun _ => _ ) in (Value of Q).
+instantiate (1:= fun _ => _ ) in (Value of Q).
+instantiate (1:= H) in (Value of Q).