Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr//gitroot/coq/coq into trunk

3 files changed, 9 insertions, 17 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 08643a1d9a..780da888e2 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -336,7 +336,15 @@ let push_rel_context_to_named_context env typ =
   let (subst, vsubst, _, env) =
     Context.fold_rel_context
       (fun (na,c,t) (subst, vsubst, avoid, env) ->
-	let id = next_ident_away (id_of_name_using_hdchar env t na) avoid in
+        let id =
+          (* ppedrot: we want to infer nicer names for the refine tactic, but
+             keeping at the same time backward compatibility in other code
+             using this function. For now, we only attempt to preserve the
+             old behaviour of Program, but ultimately, one should do something
+             about this whole name generation problem. *)
+          if Flags.is_program_mode () then next_name_away na avoid
+          else next_ident_away (id_of_name_using_hdchar env t na) avoid
+        in
         match extract_if_neq id na with
         | Some id0 when not (is_section_variable id0) ->
             (* spiwack: if [id<>id0], rather than introducing a new
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5537d87d03..5870a22b73 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -222,15 +222,6 @@ let eq_evar_info ei1 ei2 =
 exception NotInstantiatedEvar
 
 (* Note: let-in contributes to the instance *)
-let make_evar_instance sign args =
-  let rec instrec sign args = match sign, args with
-  | [], [] -> []
-  | (id,_,_) :: sign, c :: args ->
-    if isVarId id c then instrec sign args
-    else (id, c) :: instrec sign args
-  | [], _ | _, [] -> instance_mismatch ()
-  in
-  instrec sign args
 
 let make_evar_instance_array info args =
   let len = Array.length args in
@@ -251,12 +242,6 @@ let make_evar_instance_array info args =
   let filter = Filter.repr (evar_filter info) in
   instrec filter (evar_context info) 0
 
-let instantiate_evar sign c args =
-  let inst = make_evar_instance sign args in
-  match inst with
-  | [] -> c
-  | _ -> replace_vars inst c
-
 let instantiate_evar_array info c args =
   let inst = make_evar_instance_array info args in
   match inst with
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index ec16f53b76..58e4cd630b 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -218,7 +218,6 @@ val existential_opt_value : evar_map -> existential -> constr option
 (** Same as {!existential_value} but returns an option instead of raising an
     exception. *)
 
-val instantiate_evar : named_context -> constr -> constr list -> constr
 val instantiate_evar_array : evar_info -> constr -> constr array -> constr
 
 val subst_evar_defs_light : substitution -> evar_map -> evar_map