diff options
| author | Pierre-Marie Pédrot | 2018-06-22 12:24:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-07 16:34:44 +0200 |
| commit | ef29c0a927728d9cf4a45bc3c26d2393d753184e (patch) | |
| tree | d43b108a24ac69f7fbcdd184781141fea36a1dd5 /plugins/ltac/extraargs.mli | |
| 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/extraargs.mli')
| -rw-r--r-- | plugins/ltac/extraargs.mli | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index 7371478848..e477b12cd3 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -14,12 +14,12 @@ open Constrexpr open Glob_term val wit_orient : bool Genarg.uniform_genarg_type -val orient : bool Pcoq.Gram.entry +val orient : bool Pcoq.Entry.t val pr_orient : bool -> Pp.t val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type -val occurrences : (int list Locus.or_var) Pcoq.Gram.entry +val occurrences : (int list Locus.or_var) Pcoq.Entry.t val wit_occurrences : (int list Locus.or_var, int list Locus.or_var, int list) Genarg.genarg_type val pr_occurrences : int list Locus.or_var -> Pp.t val occurrences_of : int list -> Locus.occurrences @@ -46,8 +46,8 @@ val wit_casted_constr : Tacexpr.glob_constr_and_expr, EConstr.t) Genarg.genarg_type -val glob : constr_expr Pcoq.Gram.entry -val lglob : constr_expr Pcoq.Gram.entry +val glob : constr_expr Pcoq.Entry.t +val lglob : constr_expr Pcoq.Entry.t type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location @@ -55,10 +55,10 @@ type loc_place = lident gen_place type place = Id.t gen_place val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type -val hloc : loc_place Pcoq.Gram.entry +val hloc : loc_place Pcoq.Entry.t val pr_hloc : loc_place -> Pp.t -val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry +val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Entry.t val wit_by_arg_tac : (raw_tactic_expr option, glob_tactic_expr option, @@ -68,13 +68,13 @@ val pr_by_arg_tac : (int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) -> raw_tactic_expr option -> Pp.t -val test_lpar_id_colon : unit Pcoq.Gram.entry +val test_lpar_id_colon : unit Pcoq.Entry.t val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type (** Spiwack: Primitive for retroknowledge registration *) -val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry +val retroknowledge_field : Retroknowledge.field Pcoq.Entry.t val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type val wit_in_clause : |