diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:09:01 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:09:01 +0000 |
| commit | a3ab8b07b912afd1b883ed60bd532b5a29bccd8f (patch) | |
| tree | 8f5755d4bca03047baa9cebf41d8157b0380d92c /toplevel | |
| parent | 525090840aa3cd661bdac013860766fcc3886731 (diff) | |
Stuff about notation_constr (ex-aconstr) now in notation_ops.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15381 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |