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/ssr | |
| 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/ssr')
| -rw-r--r-- | plugins/ssr/ssrparser.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrparser.mli | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 6b183dab1..8b9c94f2d 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1408,7 +1408,7 @@ let check_seqtacarg dir arg = match snd arg, dir with CErrors.user_err ?loc (str "expected \"first\"") | _, _ -> arg -let ssrorelse = Gram.entry_create "ssrorelse" +let ssrorelse = Entry.create "ssrorelse" GEXTEND Gram GLOBAL: ssrorelse ssrseqarg; ssrseqidx: [ diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index 7cd3751ce..862a93765 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -12,11 +12,11 @@ open Ltac_plugin -val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry +val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c -val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry +val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Entry.t val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd |