diff options
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index bb5be4cb0..fb7c72941 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -192,7 +192,7 @@ let parse_format ((loc, str) : lstring) = error "Empty format." with reraise -> let (e, info) = CErrors.push reraise in - let info = Loc.add_loc info loc in + let info = Option.cata (Loc.add_loc info) info loc in iraise (e, info) (***********************) @@ -1416,7 +1416,7 @@ let add_notation_extra_printing_rule df k v = (* Infix notations *) -let inject_var x = CRef (Ident (Loc.ghost, Id.of_string x),None) +let inject_var x = CAst.make @@ CRef (Ident (Loc.tag @@ Id.of_string x),None) let add_infix local ((loc,inf),modifiers) pr sc = check_infix_modifiers modifiers; @@ -1477,7 +1477,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 + | [], { CAst.v = CRef (ref,_) } -> intern_reference ref | _ -> raise Not_found let add_syntactic_definition ident (vars,c) local onlyparse = |