diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/metasyntax.ml | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 2 |
2 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 5a305ccc9..6b64f9546 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -14,6 +14,7 @@ open Util open Names open Constrexpr open Notation_term +open Notation_ops open Topconstr open Ppextend open Extend diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 73c05de3f..4c2b2f9b2 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -875,7 +875,7 @@ let vernac_reserve bl = let sb_decl = (fun (idl,c) -> let t = Constrintern.interp_type Evd.empty (Global.env()) c in let t = Detyping.detype false [] [] t in - let t = Topconstr.notation_constr_of_glob_constr [] [] t in + let t = Notation_ops.notation_constr_of_glob_constr [] [] t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl |