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 /vernac/egramcoq.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 'vernac/egramcoq.ml')
| -rw-r--r-- | vernac/egramcoq.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 48f225f97..3281b75aa 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -240,14 +240,14 @@ type (_, _) entry = type _ any_entry = TTAny : ('s, 'r) entry -> 's any_entry (* This computes the name of the level where to add a new rule *) -let interp_constr_entry_key : type r. r target -> int -> r Gram.entry * int option = +let interp_constr_entry_key : type r. r target -> int -> r Entry.t * int option = fun forpat level -> match forpat with | ForConstr -> if level = 200 then Constr.binder_constr, None else Constr.operconstr, Some level | ForPattern -> Constr.pattern, Some level -let target_entry : type s. s target -> s Gram.entry = function +let target_entry : type s. s target -> s Entry.t = function | ForConstr -> Constr.operconstr | ForPattern -> Constr.pattern |