From b9b737fee66e954c70bbedbe67517e5b91cc0efb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 30 Nov 2013 00:20:31 +0100
Subject: Tentative fix to recover fresh name generation as it was before
 new-tacticals merge. This is essentially a revert of 6fea2f which broke the
 sacrosanct backward compatibility of name generation, thus breaking quite a
 lot of contribs.

---
 pretyping/evarutil.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 08643a1d9a..a283286478 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -336,7 +336,7 @@ 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 = next_name_away 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
-- 
cgit v1.2.3


From 2b2cb750e396f1a2e9cd96371ac7034ba34349e4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 30 Nov 2013 01:42:45 +0100
Subject: Useless instantiation function exported in Evd.

---
 pretyping/evd.ml  | 15 ---------------
 pretyping/evd.mli |  1 -
 2 files changed, 16 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3


From b86e7c1247fa4b34b75cf20ef24a8e0b6ba6eff1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 30 Nov 2013 15:50:31 +0100
Subject: Better heuristic for name generation backward compatibility. We
 fallback to old behaviour whenever we were in Program mode.

---
 pretyping/evarutil.ml | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index a283286478..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_name_away 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
-- 
cgit v1.2.3