Namegen primitives now apply on evar constrs.

Incidentally, this fixes a printing bug in output/inference.v where the
displayed name of an evar was the wrong one because its type was not
evar-expanded enough.

1 files changed, 5 insertions, 3 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 836568b890..a63264b669 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -228,10 +228,12 @@ let rec is_rigid_head t = match kind_of_term t with
 
 (* calcule la liste des arguments implicites *)
 
-let find_displayed_name_in all avoid na (_,b as envnames_b) =
+let find_displayed_name_in all avoid na (env, b) =
+  let b = EConstr.of_constr b in
+  let envnames_b = (env, b) in
   let flag = RenamingElsewhereFor envnames_b in
-  if all then compute_and_force_displayed_name_in flag avoid na b
-  else compute_displayed_name_in flag avoid na b
+  if all then compute_and_force_displayed_name_in Evd.empty flag avoid na b
+  else compute_displayed_name_in Evd.empty flag avoid na b
 
 let compute_implicits_gen strict strongly_strict revpat contextual all env t =
   let rigid = ref true in