From be51c33a6bf91a00fdd5f3638ddb5b3cc3a2c626 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Nov 2016 00:41:31 +0100 Subject: 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. --- interp/notation_ops.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'interp/notation_ops.ml') diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 7dbd94aa7..549e8e787 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; -- cgit v1.2.3