diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-20 17:10:58 +0200 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-25 16:07:32 +0200 |
commit | fc218c26cfb226be25c344af50b4b86e52360934 (patch) | |
tree | fd0650fa1fc981c81e62991d8d8e97431312285e /grammar/q_util.mlp | |
parent | b6f3c8e4f173e3f272f966e1061e7112bf5d1b4a (diff) |
[api] Remove type equalities from API.
This ensures that the API is self-contained and is, well, an API.
Before this patch, the contents of `API.mli` bore little relation with
what was used by the plugins [example: `Metasyntax` in tacentries.ml].
Many missing types had to be added.
A sanity check of the `API.mli` file can be done with:
`ocamlfind ocamlc -rectypes -package camlp5 -I lib API/API.mli`
Diffstat (limited to 'grammar/q_util.mlp')
-rw-r--r-- | grammar/q_util.mlp | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 51a4c3573..536ee7ca5 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -57,23 +57,23 @@ let mlexpr_of_option f = function | Some e -> <:expr< Some $f e$ >> let mlexpr_of_name f = function - | None -> <:expr< API.Names.Name.Anonymous >> - | Some e -> <:expr< API.Names.Name.Name $f e$ >> + | None -> <:expr< Names.Name.Anonymous >> + | Some e -> <:expr< Names.Name.Name $f e$ >> -let symbol_of_string s = <:expr< Grammar_API.Extend.Atoken (Grammar_API.CLexer.terminal $str:s$) >> +let symbol_of_string s = <:expr< Extend.Atoken (CLexer.terminal $str:s$) >> let rec mlexpr_of_prod_entry_key f = function - | Ulist1 s -> <:expr< Grammar_API.Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> - | Ulist1sep (s,sep) -> <:expr< Grammar_API.Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> - | Ulist0 s -> <:expr< Grammar_API.Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> - | Ulist0sep (s,sep) -> <:expr< Grammar_API.Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> - | Uopt s -> <:expr< Grammar_API.Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> - | Uentry e -> <:expr< Grammar_API.Extend.Aentry ($f e$) >> + | Ulist1 s -> <:expr< Extend.Alist1 $mlexpr_of_prod_entry_key f s$ >> + | Ulist1sep (s,sep) -> <:expr< Extend.Alist1sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> + | Ulist0 s -> <:expr< Extend.Alist0 $mlexpr_of_prod_entry_key f s$ >> + | Ulist0sep (s,sep) -> <:expr< Extend.Alist0sep $mlexpr_of_prod_entry_key f s$ $symbol_of_string sep$ >> + | Uopt s -> <:expr< Extend.Aopt $mlexpr_of_prod_entry_key f s$ >> + | Uentry e -> <:expr< Extend.Aentry ($f e$) >> | Uentryl (e, l) -> (** Keep in sync with Pcoq! *) assert (e = "tactic"); - if l = 5 then <:expr< Grammar_API.Extend.Aentry Pltac.binder_tactic >> - else <:expr< Grammar_API.Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >> + if l = 5 then <:expr< Extend.Aentry Pltac.binder_tactic >> + else <:expr< Extend.Aentryl (Pltac.tactic_expr) $mlexpr_of_int l$ >> let rec type_of_user_symbol = function | Ulist1 s | Ulist1sep (s, _) | Ulist0 s | Ulist0sep (s, _) -> |