Fixing anomaly #3743 while printing an error message involving evar constraints.

Indeed, the name of a bound variable was lost when unifying under a Prod in
evarconv.

The error message for "Unable to satisfy the following constraints" is
still to be improved though.

2 files changed, 6 insertions, 1 deletions

diff --git a/library/nameops.ml b/library/nameops.ml
index 02b085a7ac..3a23ab97df 100644
--- a/library/nameops.ml
+++ b/library/nameops.ml
@@ -136,6 +136,11 @@ let name_fold_map f e = function
   | Name id -> let (e,id) = f e id in (e,Name id)
   | Anonymous -> e,Anonymous
 
+let name_max na1 na2 =
+  match na1 with
+  | Name _ -> na1
+  | Anonymous -> na2
+
 let pr_lab l = str (Label.to_string l)
 
 let default_library = Names.DirPath.initial (* = ["Top"] *)
diff --git a/library/nameops.mli b/library/nameops.mli
index 23432ae2fa..de1f99fe0f 100644
--- a/library/nameops.mli
+++ b/library/nameops.mli
@@ -34,7 +34,7 @@ val name_iter : (Id.t -> unit) -> Name.t -> unit
 val name_cons : Name.t -> Id.t list -> Id.t list
 val name_app : (Id.t -> Id.t) -> Name.t -> Name.t
 val name_fold_map : ('a -> Id.t -> 'a * Id.t) -> 'a -> Name.t -> 'a * Name.t
-
+val name_max : Name.t -> Name.t -> Name.t
 
 val pr_lab : Label.t -> Pp.std_ppcmds