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, 1 insertions, 0 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7dbd94aa74..549e8e7879 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -441,6 +441,7 @@ let notation_constr_of_glob_constr nenv a =
 (* Substitution of kernel names, avoiding a list of bound identifiers *)
 
 let notation_constr_of_constr avoiding t =
+  let t = EConstr.of_constr t in
   let t = Detyping.detype false avoiding (Global.env()) Evd.empty t in
   let nenv = {
     ninterp_var_type = Id.Map.empty;