Merge branch 'v8.6'

3 files changed, 16 insertions, 1 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index 69ca45444c..bde0182cc5 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -643,6 +643,7 @@ let set_universe_context evd uctx' =
   { evd with universes = uctx' }
 
 let add_conv_pb ?(tail=false) pb d =
+  (** MS: we have duplicates here, why? *)
   if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
   else {d with conv_pbs = pb::d.conv_pbs}
 
@@ -1410,7 +1411,16 @@ let print_env_short env =
 
 let pr_evar_constraints pbs =
   let pr_evconstr (pbty, env, t1, t2) =
-    let env = Namegen.make_all_name_different env in
+    let env =
+      (** We currently allow evar instances to refer to anonymous de
+          Bruijn indices, so we protect the error printing code in this
+          case by giving names to every de Bruijn variable in the
+          rel_context of the conversion problem. MS: we should rather
+          stop depending on anonymous variables, they can be used to
+          indicate independency. Also, this depends on a strategy for
+          naming/renaming. *)
+      Namegen.make_all_name_different env
+    in
     print_env_short env ++ spc () ++ str "|-" ++ spc () ++
       print_constr_env env t1 ++ spc () ++
       str (match pbty with
diff --git a/engine/termops.ml b/engine/termops.ml
index 5e65652c01..5327f18296 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -600,6 +600,10 @@ let collect_vars c =
   | _ -> fold_constr aux vars c in
   aux Id.Set.empty c
 
+let vars_of_global_reference env gr =
+  let c, _ = Universes.unsafe_constr_of_global gr in
+  vars_of_global (Global.env ()) c
+
 (* Tests whether [m] is a subterm of [t]:
    [m] is appropriately lifted through abstractions of [t] *)
 
diff --git a/engine/termops.mli b/engine/termops.mli
index 7d6e99accb..c58e3728ca 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -121,6 +121,7 @@ val dependent_in_decl : constr -> Context.Named.Declaration.t -> bool
 val count_occurrences : constr -> constr -> int
 val collect_metas : constr -> int list
 val collect_vars : constr -> Id.Set.t (** for visible vars only *)
+val vars_of_global_reference : env -> Globnames.global_reference -> Id.Set.t
 val occur_term : constr -> constr -> bool (** Synonymous
  of dependent 
    Substitution of metavariables *)