From 7eeec8f82d96a71929289b0b9401a1b96e1d3dda Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Feb 2016 10:26:28 +0100
Subject: More compact representation for evar resolvability flag.

This patch was proposed by JH in bug report #4547.
---
 pretyping/typeclasses.ml | 11 +++++++----
 1 file changed, 7 insertions(+), 4 deletions(-)

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 3be98a1ae2..bb475cc554 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -495,15 +495,18 @@ let is_instance = function
 let resolvable = Store.field ()
 
 let set_resolvable s b =
-  Store.set s resolvable b
+  if b then Store.remove s resolvable
+  else Store.set s resolvable ()
 
 let is_resolvable evi =
   assert (match evi.evar_body with Evar_empty -> true | _ -> false);
-  Option.default true (Store.get evi.evar_extra resolvable)
+  Option.is_empty (Store.get evi.evar_extra resolvable)
 
 let mark_resolvability_undef b evi =
-  let t = Store.set evi.evar_extra resolvable b in
-  { evi with evar_extra = t }
+  if is_resolvable evi = b then evi
+  else
+    let t = set_resolvable evi.evar_extra b in
+    { evi with evar_extra = t }
 
 let mark_resolvability b evi =
   assert (match evi.evar_body with Evar_empty -> true | _ -> false);
-- 
cgit v1.2.3


From 0ee0b7d2f2365da6e63bc2e94d66f9c5fe1ebe6a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Feb 2016 11:28:34 +0100
Subject: Opacifying the type of evar naming structure in Evd.

---
 pretyping/evd.ml | 124 +++++++++++++++++++++++++++++++++----------------------
 1 file changed, 74 insertions(+), 50 deletions(-)

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 5441145189..8be09a7821 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -575,34 +575,28 @@ type evar_constraint = conv_pb * Environ.env * constr * constr
 
 module EvMap = Evar.Map
 
-type evar_map = {
-  (** Existential variables *)
-  defn_evars : evar_info EvMap.t;
-  undf_evars : evar_info EvMap.t;
-  evar_names : Id.t EvMap.t * existential_key Idmap.t;
-  (** Universes *)
-  universes  : evar_universe_context;
-  (** Conversion problems *)
-  conv_pbs   : evar_constraint list;
-  last_mods  : Evar.Set.t;
-  (** Metas *)
-  metas      : clbinding Metamap.t;
-  (** Interactive proofs *)
-  effects    : Safe_typing.private_constants;
-  future_goals : Evar.t list; (** list of newly created evars, to be
-                                  eventually turned into goals if not solved.*)
-  principal_future_goal : Evar.t option; (** if [Some e], [e] must be
-                                             contained
-                                             [future_goals]. The evar
-                                             [e] will inherit
-                                             properties (now: the
-                                             name) of the evar which
-                                             will be instantiated with
-                                             a term containing [e]. *)
-  extras : Store.t;
-}
+module EvNames :
+sig
 
-(*** Lifting primitive from Evar.Map. ***)
+open Misctypes
+
+type t
+
+val empty : t
+val add_name_newly_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t
+val add_name_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -> t
+val remove_name_defined : Evar.t -> t -> t
+val rename : Evar.t -> Id.t -> t -> t
+val reassign_name_defined : Evar.t -> Evar.t -> t -> t
+val ident : Evar.t -> t -> Id.t
+val key : Id.t -> t -> Evar.t
+
+end =
+struct
+
+type t = Id.t EvMap.t * existential_key Idmap.t
+
+let empty = (EvMap.empty, Idmap.empty)
 
 let add_name_newly_undefined naming evk evi (evtoid,idtoev) =
   let id = match naming with
@@ -630,29 +624,65 @@ let remove_name_defined evk (evtoid,idtoev) =
   let id = EvMap.find evk evtoid in
   (EvMap.remove evk evtoid, Idmap.remove id idtoev)
 
-let remove_name_possibly_already_defined evk evar_names =
-  try remove_name_defined evk evar_names
-  with Not_found -> evar_names
-
-let rename evk id evd =
-  let (evtoid,idtoev) = evd.evar_names in
+let rename evk id (evtoid, idtoev) =
   let id' = EvMap.find evk evtoid in
   if Idmap.mem id idtoev then anomaly (str "Evar name already in use");
-  { evd with evar_names =
-      (EvMap.add evk id evtoid (* overwrite old name *),
-       Idmap.add id evk (Idmap.remove id' idtoev)) }
+  (EvMap.add evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev))
 
 let reassign_name_defined evk evk' (evtoid,idtoev) =
   let id = EvMap.find evk evtoid in
   (EvMap.add evk' id (EvMap.remove evk evtoid),
    Idmap.add id evk' (Idmap.remove id idtoev))
 
+let ident evk (evtoid, _) =
+  try EvMap.find evk evtoid
+  with Not_found ->
+    (* Unnamed (non-dependent) evar *)
+    add_suffix (Id.of_string "X") (string_of_int (Evar.repr evk))
+
+let key id (_, idtoev) =
+  Idmap.find id idtoev
+
+end
+
+type evar_map = {
+  (** Existential variables *)
+  defn_evars : evar_info EvMap.t;
+  undf_evars : evar_info EvMap.t;
+  evar_names : EvNames.t;
+  (** Universes *)
+  universes  : evar_universe_context;
+  (** Conversion problems *)
+  conv_pbs   : evar_constraint list;
+  last_mods  : Evar.Set.t;
+  (** Metas *)
+  metas      : clbinding Metamap.t;
+  (** Interactive proofs *)
+  effects    : Safe_typing.private_constants;
+  future_goals : Evar.t list; (** list of newly created evars, to be
+                                  eventually turned into goals if not solved.*)
+  principal_future_goal : Evar.t option; (** if [Some e], [e] must be
+                                             contained
+                                             [future_goals]. The evar
+                                             [e] will inherit
+                                             properties (now: the
+                                             name) of the evar which
+                                             will be instantiated with
+                                             a term containing [e]. *)
+  extras : Store.t;
+}
+
+(*** Lifting primitive from Evar.Map. ***)
+
+let rename evk id evd =
+  { evd with evar_names = EvNames.rename evk id evd.evar_names }
+
 let add d e i = match i.evar_body with
 | Evar_empty ->
-  let evar_names = add_name_undefined Misctypes.IntroAnonymous e i d.evar_names in
+  let evar_names = EvNames.add_name_undefined Misctypes.IntroAnonymous e i d.evar_names in
   { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
 | Evar_defined _ ->
-  let evar_names = remove_name_possibly_already_defined e d.evar_names in
+  let evar_names = try EvNames.remove_name_defined e d.evar_names with Not_found -> d.evar_names in
   { d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
 
 let remove d e =
@@ -783,7 +813,7 @@ let empty = {
   last_mods  = Evar.Set.empty;
   metas      = Metamap.empty;
   effects    = Safe_typing.empty_private_constants;
-  evar_names = (EvMap.empty,Idmap.empty); (* id<->key for undefined evars *)
+  evar_names = EvNames.empty; (* id<->key for undefined evars *)
   future_goals = [];
   principal_future_goal = None;
   extras = Store.empty;
@@ -819,14 +849,8 @@ let add_conv_pb ?(tail=false) pb d =
 
 let evar_source evk d = (find d evk).evar_source
 
-let evar_ident evk evd =
-  try EvMap.find evk (fst evd.evar_names)
-  with Not_found ->
-    (* Unnamed (non-dependent) evar *)
-    add_suffix (Id.of_string "X") (string_of_int (Evar.repr evk))
-
-let evar_key id evd =
-  Idmap.find id (snd evd.evar_names)
+let evar_ident evk evd = EvNames.ident evk evd.evar_names
+let evar_key id evd = EvNames.key id evd.evar_names
 
 let define_aux def undef evk body =
   let oldinfo =
@@ -848,7 +872,7 @@ let define evk body evd =
   | [] ->  evd.last_mods
   | _ -> Evar.Set.add evk evd.last_mods
   in
-  let evar_names = remove_name_defined evk evd.evar_names in
+  let evar_names = EvNames.remove_name_defined evk evd.evar_names in
   { evd with defn_evars; undf_evars; last_mods; evar_names }
 
 let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole)) 
@@ -868,7 +892,7 @@ let evar_declare hyps evk ty ?(src=(Loc.ghost,Evar_kinds.InternalHole))
     evar_candidates = candidates;
     evar_extra = store; }
   in
-  let evar_names = add_name_newly_undefined naming evk evar_info evd.evar_names in
+  let evar_names = EvNames.add_name_newly_undefined naming evk evar_info evd.evar_names in
   { evd with undf_evars = EvMap.add evk evar_info evd.undf_evars; evar_names }
 
 let restrict evk evk' filter ?candidates evd =
@@ -877,7 +901,7 @@ let restrict evk evk' filter ?candidates evd =
     { evar_info with evar_filter = filter;
       evar_candidates = candidates;
       evar_extra = Store.empty } in
-  let evar_names = reassign_name_defined evk evk' evd.evar_names in
+  let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
   let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) ctxt in
   let body = mkEvar(evk',id_inst) in
-- 
cgit v1.2.3


From 62c141be71dd3c542824c19429eac0fdd686c9cb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Feb 2016 18:39:15 +0100
Subject: Optimizing the computation of frozen evars.

---
 pretyping/unification.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index f97f6fbc57..6cb1bc7028 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1450,9 +1450,7 @@ let default_matching_core_flags sigma =
   check_applied_meta_types = true;
   use_pattern_unification = false;
   use_meta_bound_pattern_unification = false;
-  frozen_evars =
-    fold_undefined (fun evk _ evars -> Evar.Set.add evk evars)
-      sigma Evar.Set.empty;
+  frozen_evars = Evar.Map.domain (Evd.undefined_map sigma);
   restrict_conv_on_strict_subterms = false;
   modulo_betaiota = false;
   modulo_eta = false;
-- 
cgit v1.2.3


From 5d9eaa378277ed96456fec5a2037a8da4f38c8e0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Feb 2016 20:07:33 +0100
Subject: Optimizing the universes_of_constr_function.

Instead of relying on a costly set union, we take advantage of the fact
that instances are small compared to the set of universes.
---
 library/universes.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/universes.ml b/library/universes.ml
index 7972c478ad..3bebdafc78 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -959,10 +959,10 @@ let universes_of_constr c =
   let rec aux s c = 
     match kind_of_term c with
     | Const (_, u) | Ind (_, u) | Construct (_, u) ->
-      LSet.union (Instance.levels u) s
+      LSet.fold LSet.add (Instance.levels u) s
     | Sort u when not (Sorts.is_small u) -> 
       let u = univ_of_sort u in
-	LSet.union (Universe.levels u) s
+      LSet.fold LSet.add (Universe.levels u) s
     | _ -> fold_constr aux s c
   in aux LSet.empty c
 
-- 
cgit v1.2.3


From 68db732f12980e592c610085192d93457f312607 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 8 Feb 2016 11:19:09 +0100
Subject: Improving error message with missing patterns in the presence of
 multiple patterns.

---
 toplevel/himsg.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 89c33cb6fe..c0a99fe75c 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1207,7 +1207,7 @@ let explain_unused_clause env pats =
 let explain_non_exhaustive env pats =
   str "Non exhaustive pattern-matching: no clause found for " ++
   str (String.plural (List.length pats) "pattern") ++
-  spc () ++ hov 0 (pr_sequence pr_cases_pattern pats)
+  spc () ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats)
 
 let explain_cannot_infer_predicate env sigma typs =
   let env = make_all_name_different env in
-- 
cgit v1.2.3


From 5f29a92c0648afd4d9e46de79ab00d0c4b901ff0 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 9 Feb 2016 16:36:05 +0100
Subject: Don't fail fatally if PATH is not set.

This fixes micromega in certain environments.
---
 lib/system.ml | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/lib/system.ml b/lib/system.ml
index 9bdcecef19..0ad43a7423 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -149,10 +149,12 @@ let is_in_path lpath filename =
   with Not_found -> false
 
 let is_in_system_path filename =
-  let path = try Sys.getenv "PATH"
-             with Not_found -> error "system variable PATH not found" in
-  let lpath = CUnix.path_to_list path in
-  is_in_path lpath filename
+  try
+    let lpath = CUnix.path_to_list (Sys.getenv "PATH") in
+    is_in_path lpath filename
+  with Not_found ->
+    msg_warning (str "system variable PATH not found");
+    false
 
 let open_trapping_failure name =
   try open_out_bin name
-- 
cgit v1.2.3


From 22ab7fff908c259d6e433da246bebac519009905 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 10 Feb 2016 17:54:25 +0100
Subject: STM: not delegate proofs that contain Vernac(Module|Require|Import),
 #4530

---
 stm/stm.ml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/stm/stm.ml b/stm/stm.ml
index d8b2de4a2c..5ad1aead61 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1686,6 +1686,13 @@ let collect_proof keep cur hd brkind id =
    | _ -> false in
  let may_pierce_opaque = function
    | { expr = VernacPrint (PrintName _) } -> true
+   (* These do not exactly pierce opaque, but are anyway impossible to properly
+    * delegate *)
+   | { expr = (VernacDeclareModule _
+              | VernacDefineModule _
+              | VernacDeclareModuleType _
+              | VernacInclude _) } -> true
+   | { expr =  (VernacRequire _ | VernacImport _) } -> true
    | _ -> false in
  let parent = function Some (p, _) -> p | None -> assert false in
  let is_empty = function `Async(_,_,[],_,_) | `MaybeASync(_,_,[],_,_) -> true | _ -> false in
-- 
cgit v1.2.3


From df6bb883920e3a03044d09f10b57a44a2e7c5196 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 10 Feb 2016 17:59:14 +0100
Subject: STM: always stock in vio files the first node (state) of a proof

It used not to be the case when the proof contains Sideff, since
the code was picking the last known state and not necessarily the
first one.  Because of side effects the last known state could be
the one corresponding to the side effect (that was executed to, say,
change the parser).  This is also related to bug #4530
---
 stm/stm.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/stm/stm.ml b/stm/stm.ml
index 5ad1aead61..56dcda6a4a 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -513,7 +513,10 @@ end = struct (* {{{ *)
     let rec fill id =
       if (get_info id).state = None then fill (Vcs_aux.visit v id).next
       else copy_info_w_state v id in
-    fill stop
+    let v = fill stop in
+    (* We put in the new dag the first state (since Qed shall run on it,
+     * see check_task_aux) *)
+    copy_info_w_state v start
 
   let nodes_in_slice ~start ~stop =
     List.rev (List.map fst (nodes_in_slice ~start ~stop))
-- 
cgit v1.2.3


From f46a5686853353f8de733ae7fbd21a3a61977bc7 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 3 Feb 2016 15:32:58 +0100
Subject: Do not give a name to anonymous evars anymore. See bug #4547.

The current solution may not be totally ideal though. We generate names for
anonymous evars on the fly at printing time, based on the Evar_kind data they
are wearing. This means in particular that the printed name of an anonymous
evar may change in the future because some unrelate evar has been solved or
introduced.
---
 interp/constrextern.ml             |   5 +-
 pretyping/detyping.ml              |   5 +-
 pretyping/evarutil.ml              |   9 +---
 pretyping/evd.ml                   | 103 +++++++++++++++++++++++--------------
 pretyping/evd.mli                  |   4 +-
 printing/printer.ml                |   2 +-
 proofs/goal.ml                     |   5 +-
 proofs/proofview.ml                |   5 +-
 test-suite/bugs/closed/3068.v      |   2 +-
 test-suite/output/Existentials.out |   3 +-
 test-suite/output/Notations.out    |  14 ++---
 test-suite/output/inference.out    |   8 +--
 test-suite/success/apply.v         |   2 +-
 test-suite/success/destruct.v      |   8 +--
 14 files changed, 102 insertions(+), 73 deletions(-)

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9df8f9c233..cc5d189e04 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -988,7 +988,10 @@ let rec glob_of_pat env sigma = function
   | PEvar (evk,l) ->
       let test (id,_,_) = function PVar id' -> Id.equal id id' | _ -> false in
       let l = Evd.evar_instance_array test (Evd.find sigma evk) l in
-      let id = Evd.evar_ident evk sigma in
+      let id = match Evd.evar_ident evk sigma with
+      | None -> Id.of_string "__"
+      | Some id -> id
+      in
       GEvar (loc,id,List.map (on_snd (glob_of_pat env sigma)) l)
   | PRel n ->
       let id = try match lookup_name_of_rel n env with
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c3877c56e4..0c487ced81 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -518,7 +518,10 @@ let rec detype flags avoid env sigma t =
 	  with Not_found -> isVarId id c in
       let id,l =
         try
-          let id = Evd.evar_ident evk sigma in
+          let id = match Evd.evar_ident evk sigma with
+          | None -> Evd.pr_evar_suggested_name evk sigma
+          | Some id -> id
+          in
           let l = Evd.evar_instance_array bound_to_itself_or_letin (Evd.find sigma evk) cl in
           let fvs,rels = List.fold_left (fun (fvs,rels) (_,c) -> match kind_of_term c with Rel n -> (fvs,Int.Set.add n rels) | Var id -> (Id.Set.add id fvs,rels) | _ -> (fvs,rels)) (Id.Set.empty,Int.Set.empty) l in
           let l = Evd.evar_instance_array (fun d c -> not !print_evar_arguments && (bound_to_itself_or_letin d c && not (isRel c && Int.Set.mem (destRel c) rels || isVar c && (Id.Set.mem (destVar c) fvs)))) (Evd.find sigma evk) cl in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index e23e5a53a7..759e0e4d6d 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -365,14 +365,7 @@ let new_pure_evar_full evd evi =
   (evd, evk)
 
 let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?naming ?(principal=false) typ =
-  let default_naming =
-    if principal then
-        (* waiting for a more principled approach
-           (unnamed evars, private names?) *)
-        Misctypes.IntroFresh (Names.Id.of_string "tmp_goal")
-      else
-        Misctypes.IntroAnonymous
-  in
+  let default_naming = Misctypes.IntroAnonymous in
   let naming = Option.default default_naming naming in
   let newevk = new_untyped_evar() in
   let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store ~naming evd in
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 8be09a7821..0bc688aacf 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -208,15 +208,6 @@ let map_evar_info f evi =
     evar_concl = f evi.evar_concl;
     evar_candidates = Option.map (List.map f) evi.evar_candidates }
 
-let evar_ident_info evi =
-  match evi.evar_source with
-  | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
-  | _,Evar_kinds.VarInstance id -> id
-  | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
-  | _ ->
-      let env = reset_with_named_context evi.evar_hyps (Global.env()) in
-      Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
-
 (* This exception is raised by *.existential_value *)
 exception NotInstantiatedEvar
 
@@ -588,7 +579,7 @@ val add_name_undefined : intro_pattern_naming_expr -> Evar.t -> evar_info -> t -
 val remove_name_defined : Evar.t -> t -> t
 val rename : Evar.t -> Id.t -> t -> t
 val reassign_name_defined : Evar.t -> Evar.t -> t -> t
-val ident : Evar.t -> t -> Id.t
+val ident : Evar.t -> t -> Id.t option
 val key : Id.t -> t -> Evar.t
 
 end =
@@ -598,21 +589,21 @@ type t = Id.t EvMap.t * existential_key Idmap.t
 
 let empty = (EvMap.empty, Idmap.empty)
 
-let add_name_newly_undefined naming evk evi (evtoid,idtoev) =
+let add_name_newly_undefined naming evk evi (evtoid, idtoev as names) =
   let id = match naming with
-  | Misctypes.IntroAnonymous ->
-      let id = evar_ident_info evi in
-      Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev)
+  | Misctypes.IntroAnonymous -> None
   | Misctypes.IntroIdentifier id ->
-      let id' =
-        Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
-      if not (Names.Id.equal id id') then
-        user_err_loc
-          (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id);
-      id'
+    if Idmap.mem id idtoev then
+    user_err_loc
+      (Loc.ghost,"",str "Already an existential evar of name " ++ pr_id id);
+    Some id
   | Misctypes.IntroFresh id ->
-      Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
-  (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+    let id = Namegen.next_ident_away_from id (fun id -> Idmap.mem id idtoev) in
+    Some id
+  in
+  match id with
+  | None -> names
+  | Some id -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
 
 let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
   if EvMap.mem evk evtoid then
@@ -620,25 +611,30 @@ let add_name_undefined naming evk evi (evtoid,idtoev as evar_names) =
   else
     add_name_newly_undefined naming evk evi evar_names
 
-let remove_name_defined evk (evtoid,idtoev) =
-  let id = EvMap.find evk evtoid in
-  (EvMap.remove evk evtoid, Idmap.remove id idtoev)
+let remove_name_defined evk (evtoid, idtoev as names) =
+  let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
+  match id with
+  | None -> names
+  | Some id -> (EvMap.remove evk evtoid, Idmap.remove id idtoev)
 
 let rename evk id (evtoid, idtoev) =
-  let id' = EvMap.find evk evtoid in
-  if Idmap.mem id idtoev then anomaly (str "Evar name already in use");
-  (EvMap.add evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev))
-
-let reassign_name_defined evk evk' (evtoid,idtoev) =
-  let id = EvMap.find evk evtoid in
-  (EvMap.add evk' id (EvMap.remove evk evtoid),
-   Idmap.add id evk' (Idmap.remove id idtoev))
+  let id' = try Some (EvMap.find evk evtoid) with Not_found -> None in
+  match id' with
+  | None -> (EvMap.add evk id evtoid, Idmap.add id evk idtoev)
+  | Some id' ->
+    if Idmap.mem id idtoev then anomaly (str "Evar name already in use");
+    (EvMap.update evk id evtoid (* overwrite old name *), Idmap.add id evk (Idmap.remove id' idtoev))
+
+let reassign_name_defined evk evk' (evtoid, idtoev as names) =
+  let id = try Some (EvMap.find evk evtoid) with Not_found -> None in
+  match id with
+  | None -> names (** evk' must not be defined *)
+  | Some id ->
+    (EvMap.add evk' id (EvMap.remove evk evtoid),
+    Idmap.add id evk' (Idmap.remove id idtoev))
 
 let ident evk (evtoid, _) =
-  try EvMap.find evk evtoid
-  with Not_found ->
-    (* Unnamed (non-dependent) evar *)
-    add_suffix (Id.of_string "X") (string_of_int (Evar.repr evk))
+  try Some (EvMap.find evk evtoid) with Not_found -> None
 
 let key id (_, idtoev) =
   Idmap.find id idtoev
@@ -682,7 +678,7 @@ let add d e i = match i.evar_body with
   let evar_names = EvNames.add_name_undefined Misctypes.IntroAnonymous e i d.evar_names in
   { d with undf_evars = EvMap.add e i d.undf_evars; evar_names }
 | Evar_defined _ ->
-  let evar_names = try EvNames.remove_name_defined e d.evar_names with Not_found -> d.evar_names in
+  let evar_names = EvNames.remove_name_defined e d.evar_names in
   { d with defn_evars = EvMap.add e i d.defn_evars; evar_names }
 
 let remove d e =
@@ -1706,7 +1702,34 @@ type unsolvability_explanation = SeveralInstancesFound of int
 (**********************************************************)
 (* Pretty-printing *)
 
-let pr_existential_key sigma evk = str "?" ++ pr_id (evar_ident evk sigma)
+let pr_evar_suggested_name evk sigma =
+  let base_id evk' evi =
+  match evar_ident evk' sigma with
+  | Some id -> id
+  | None -> match evi.evar_source with
+  | _,Evar_kinds.ImplicitArg (c,(n,Some id),b) -> id
+  | _,Evar_kinds.VarInstance id -> id
+  | _,Evar_kinds.GoalEvar -> Id.of_string "Goal"
+  | _ ->
+      let env = reset_with_named_context evi.evar_hyps (Global.env()) in
+      Namegen.id_of_name_using_hdchar env evi.evar_concl Anonymous
+  in
+  let names = EvMap.mapi base_id sigma.undf_evars in
+  let id = EvMap.find evk names in
+  let fold evk' id' (seen, n) =
+    if seen then (seen, n)
+    else if Evar.equal evk evk' then (true, n)
+    else if Id.equal id id' then (seen, succ n)
+    else (seen, n)
+  in
+  let (_, n) = EvMap.fold fold names (false, 0) in
+  if n = 0 then id else Nameops.add_suffix id (string_of_int (pred n))
+
+let pr_existential_key sigma evk = match evar_ident evk sigma with
+| None ->
+  str "?" ++ pr_id (pr_evar_suggested_name evk sigma)
+| Some id ->
+  str "?" ++ pr_id id
 
 let pr_instance_status (sc,typ) =
   begin match sc with
@@ -1895,7 +1918,7 @@ let pr_evar_list sigma l =
     h 0 (str (string_of_existential ev) ++
       str "==" ++ pr_evar_info evi ++
       (if evi.evar_body == Evar_empty
-       then str " {" ++ pr_id (evar_ident ev sigma) ++ str "}"
+       then str " {" ++  pr_existential_key sigma ev ++ str "}"
        else mt ()))
   in
   h 0 (prlist_with_sep fnl pr l)
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 9cfca02ed8..d2479c1229 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -249,7 +249,7 @@ val evar_source : existential_key -> evar_map -> Evar_kinds.t located
 (** Convenience function. Wrapper around {!find} to recover the source of an
     evar in a given evar map. *)
 
-val evar_ident : existential_key -> evar_map -> Id.t
+val evar_ident : existential_key -> evar_map -> Id.t option
 
 val rename : existential_key -> Id.t -> evar_map -> evar_map
 
@@ -603,6 +603,8 @@ type unsolvability_explanation = SeveralInstancesFound of int
 
 val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds
 
+val pr_evar_suggested_name : existential_key -> evar_map -> Id.t
+
 (** {5 Debug pretty-printers} *)
 
 val pr_evar_info : evar_info -> Pp.std_ppcmds
diff --git a/printing/printer.ml b/printing/printer.ml
index 5ad0e45319..63755d7ff7 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -400,7 +400,7 @@ let display_name = false
 
 (* display a goal name *)
 let pr_goal_name sigma g =
-  if display_name then str " " ++ Pp.surround (pr_id (Evd.evar_ident g sigma))
+  if display_name then str " " ++ Pp.surround (pr_existential_key sigma g)
   else mt ()
 
 (* display the conclusion of a goal *)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 1dd5be0e71..43a3024e50 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -89,7 +89,10 @@ module V82 = struct
   (* Instantiates a goal with an open term, using name of goal for evk' *)
   let partial_solution_to sigma evk evk' c =
     let id = Evd.evar_ident evk sigma in
-    Evd.rename evk' id (partial_solution sigma evk c)
+    let sigma = partial_solution sigma evk c in
+    match id with
+    | None -> sigma
+    | Some id -> Evd.rename evk' id sigma
 
   (* Parts of the progress tactical *)
   let same_goal evars1 gl1 evars2 gl2 =
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index a6d9735f14..49228c93ac 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -1093,7 +1093,10 @@ struct
       | None -> Evd.define gl.Goal.self c sigma
       | Some evk ->
           let id = Evd.evar_ident gl.Goal.self sigma in
-          Evd.rename evk id (Evd.define gl.Goal.self c sigma)
+          let sigma = Evd.define gl.Goal.self c sigma in
+          match id with
+          | None -> sigma
+          | Some id -> Evd.rename evk id sigma
     in
     (** Restore the [future goals] state. *)
     let sigma = Evd.restore_future_goals sigma prev_future_goals prev_principal_goal in
diff --git a/test-suite/bugs/closed/3068.v b/test-suite/bugs/closed/3068.v
index ced6d95949..79671ce930 100644
--- a/test-suite/bugs/closed/3068.v
+++ b/test-suite/bugs/closed/3068.v
@@ -56,7 +56,7 @@ Section Finite_nat_set.
       subst fs1.
       apply iff_refl.
     intros H.
-    eapply counted_list_equal_nth_char.
+    eapply (counted_list_equal_nth_char _ _ _ _ ?[def]).
     intros i.
     destruct (counted_def_nth fs1 i _ ) eqn:H0.
     (* This was not part of the initial bug report; this is to check that
diff --git a/test-suite/output/Existentials.out b/test-suite/output/Existentials.out
index 52e1e0ed01..9680d2bbff 100644
--- a/test-suite/output/Existentials.out
+++ b/test-suite/output/Existentials.out
@@ -1,5 +1,4 @@
-Existential 1 =
-?Goal1 : [p : nat  q := S p : nat  n : nat  m : nat |- ?y = m] 
+Existential 1 = ?Goal : [p : nat  q := S p : nat  n : nat  m : nat |- ?y = m] 
 Existential 2 =
 ?y : [p : nat  q := S p : nat  n : nat  m : nat |- nat] (p, q cannot be used)
 Existential 3 = ?Goal0 : [q : nat  n : nat  m : nat |- n = ?y] 
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index b1558dab1c..26eaca8272 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -111,14 +111,14 @@ fun x : option Z => match x with
                     | NONE2 => 0
                     end
      : option Z -> Z
-fun x : list ?T1 => match x with
-                    | NIL => NONE2
-                    | (_ :') t => SOME2 t
-                    end
-     : list ?T1 -> option (list ?T1)
+fun x : list ?T => match x with
+                   | NIL => NONE2
+                   | (_ :') t => SOME2 t
+                   end
+     : list ?T -> option (list ?T)
 where
-?T1 : [x : list ?T1  x1 : list ?T1  x0 := x1 : list ?T1 |- Type] (x, x1,
-      x0 cannot be used)
+?T : [x : list ?T  x1 : list ?T  x0 := x1 : list ?T |- Type] (x, x1,
+     x0 cannot be used)
 s
      : s
 10
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index f2d1447785..4512e2c5ce 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -9,10 +9,10 @@ fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
 fun n : nat => let x := A n in ?y ?y0 : T n
      : forall n : nat, T n
 where
-?y : [n : nat  x := A n : T n |- ?T0 -> T n] 
-?y0 : [n : nat  x := A n : T n |- ?T0] 
+?y : [n : nat  x := A n : T n |- ?T -> T n] 
+?y0 : [n : nat  x := A n : T n |- ?T] 
 fun n : nat => ?y ?y0 : T n
      : forall n : nat, T n
 where
-?y : [n : nat |- ?T0 -> T n] 
-?y0 : [n : nat |- ?T0] 
+?y : [n : nat |- ?T -> T n] 
+?y0 : [n : nat |- ?T] 
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 55b666b723..02e043bc36 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -543,7 +543,7 @@ Qed.
 Lemma bar (X: nat -> nat -> Prop) (foo:forall x, X x x) (a: unit) (H: tt = a):
   exists x, exists y, X x y.
 Proof.
-intros; eexists; eexists; case H.
+intros; eexists; eexists ?[y]; case H.
 apply (foo ?y).
 Grab Existential Variables.
 exact 0.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 9f091e3996..90a60daa66 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -96,21 +96,21 @@ Abort.
 (* Check that subterm selection does not solve existing evars *)
 
 Goal exists x, S x = S 0.
-eexists.
+eexists ?[x].
 Show x.  (* Incidentally test Show on a named goal *)
 destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
 change (0 = S 0).
 Abort.
 
 Goal exists x, S 0 = S x.
-eexists.
+eexists ?[x].
 destruct (S _). (* Incompatible occurrences but takes the first one since Oct 2014 *)
 change (0 = S ?x).
 [x]: exact 0. (* Incidentally test applying a tactic to a goal on the shelve *)
 Abort.
 
 Goal exists n p:nat, (S n,S n) = (S p,S p) /\ p = n.
-do 2 eexists.
+eexists ?[n]; eexists ?[p].
 destruct (_, S _). (* Was unifying at some time in trunk, now takes the first occurrence *)
 change ((n, n0) = (S ?p, S ?p) /\ ?p = ?n).
 Abort.
@@ -426,7 +426,7 @@ destruct b eqn:H.
 (* Check natural instantiation behavior when the goal has already an evar *)
 
 Goal exists x, S x = x.
-eexists.
+eexists ?[x].
 destruct (S _).
 change (0 = ?x).
 Abort.
-- 
cgit v1.2.3