diff options
Diffstat (limited to 'toplevel/metasyntax.ml')
| -rw-r--r-- | toplevel/metasyntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 761f9c214b..3b86cf72f8 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -1269,7 +1269,7 @@ let add_notation local c ((loc,df),modifiers) sc = (* Infix notations *) -let inject_var x = CRef (Ident (Loc.ghost, Id.of_string x)) +let inject_var x = CRef (Ident (Loc.ghost, Id.of_string x),None) let add_infix local ((loc,inf),modifiers) pr sc = check_infix_modifiers modifiers; @@ -1323,7 +1323,7 @@ let add_class_scope scope cl = (* Check if abbreviation to a name and avoid early insertion of maximal implicit arguments *) let try_interp_name_alias = function - | [], CRef ref -> intern_reference ref + | [], CRef (ref,_) -> intern_reference ref | _ -> raise Not_found let add_syntactic_definition ident (vars,c) local onlyparse = |