diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 59625426f0..8b4fadb5a0 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -442,6 +442,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; |