diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-22 12:24:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-07-07 16:34:44 +0200 |
| commit | ef29c0a927728d9cf4a45bc3c26d2393d753184e (patch) | |
| tree | d43b108a24ac69f7fbcdd184781141fea36a1dd5 /plugins/ltac/pltac.ml | |
| parent | 4b3187a635864f8faa2d512775231a4e6d204c51 (diff) | |
Introduce a Pcoq.Entry module for functions that ought to be exported.
We deprecate the corresponding functions in Pcoq.Gram. The motivation is
that the Gram module is used as an argument to Camlp5 functors, so that
it is not stable by extension. Enforcing that its type is literally the
one Camlp5 expects ensures robustness to extension statically.
Some really internal functions have been bluntly removed. It is unlikely
that they are used by external plugins.
Diffstat (limited to 'plugins/ltac/pltac.ml')
| -rw-r--r-- | plugins/ltac/pltac.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/plugins/ltac/pltac.ml b/plugins/ltac/pltac.ml index e9711268c..759bb62fd 100644 --- a/plugins/ltac/pltac.ml +++ b/plugins/ltac/pltac.ml @@ -11,11 +11,10 @@ open Pcoq (* Main entry for extensions *) -let simple_tactic = Gram.entry_create "tactic:simple_tactic" +let simple_tactic = Entry.create "tactic:simple_tactic" -let make_gen_entry _ name = Gram.entry_create ("tactic:" ^ name) +let make_gen_entry _ name = Entry.create ("tactic:" ^ name) -(* Entries that can be referred via the string -> Gram.entry table *) (* Typically for tactic user extensions *) let open_constr = make_gen_entry utactic "open_constr" @@ -23,7 +22,7 @@ let constr_with_bindings = make_gen_entry utactic "constr_with_bindings" let bindings = make_gen_entry utactic "bindings" -let hypident = Gram.entry_create "hypident" +let hypident = Entry.create "hypident" let constr_may_eval = make_gen_entry utactic "constr_may_eval" let constr_eval = make_gen_entry utactic "constr_eval" let uconstr = @@ -40,7 +39,7 @@ let clause_dft_concl = (* Main entries for ltac *) -let tactic_arg = Gram.entry_create "tactic:tactic_arg" +let tactic_arg = Entry.create "tactic:tactic_arg" let tactic_expr = make_gen_entry utactic "tactic_expr" let binder_tactic = make_gen_entry utactic "binder_tactic" |