diff options
Diffstat (limited to 'plugins/ltac/extraargs.mli')
| -rw-r--r-- | plugins/ltac/extraargs.mli | 23 |
1 files changed, 11 insertions, 12 deletions
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index e5a4f090..e477b12c 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -12,17 +12,16 @@ open Tacexpr open Names open Constrexpr open Glob_term -open Misctypes 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 or_var) Pcoq.Gram.entry -val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type -val pr_occurrences : int list or_var -> Pp.t +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 val wit_natural : int Genarg.uniform_genarg_type @@ -47,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 @@ -56,26 +55,26 @@ 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, Geninterp.Val.t option) Genarg.genarg_type val pr_by_arg_tac : - (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) -> + (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 : |