diff options
Diffstat (limited to 'parsing/pcoq.mli')
| -rw-r--r-- | parsing/pcoq.mli | 75 |
1 files changed, 45 insertions, 30 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 681a6b2c..44a3686e 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: pcoq.mli 10185 2007-10-06 18:05:13Z herbelin $ i*) +(*i $Id: pcoq.mli 10987 2008-05-26 12:28:36Z herbelin $ i*) open Util open Names @@ -37,10 +37,11 @@ val object_of_typed_entry : typed_entry -> grammar_object Gram.Entry.e val weaken_entry : 'a Gram.Entry.e -> grammar_object Gram.Entry.e val get_constr_entry : - bool -> constr_entry -> grammar_object Gram.Entry.e * int option * bool + bool -> constr_entry -> grammar_object Gram.Entry.e * int option val grammar_extend : - grammar_object Gram.Entry.e -> Gramext.position option -> + grammar_object Gram.Entry.e -> Gramext.position option -> + (* for reinitialization if ever: *) Gramext.g_assoc option -> (string option * Gramext.g_assoc option * (Compat.token Gramext.g_symbol list * Gramext.g_action) list) list -> unit @@ -77,7 +78,7 @@ val force_entry_type : val create_constr_entry : string * gram_universe -> string -> constr_expr Gram.Entry.e -val create_generic_entry : string -> ('a, rlevel,raw_tactic_expr) abstract_argument_type -> 'a Gram.Entry.e +val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> 'a Gram.Entry.e val get_generic_entry : string -> grammar_object Gram.Entry.e val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument_type @@ -85,33 +86,33 @@ val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument val tactic_main_level : int -val rawwit_tactic : int -> (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type -val globwit_tactic : int -> (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type -val wit_tactic : int -> (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type +val rawwit_tactic : int -> (raw_tactic_expr,rlevel) abstract_argument_type +val globwit_tactic : int -> (glob_tactic_expr,glevel) abstract_argument_type +val wit_tactic : int -> (glob_tactic_expr,tlevel) abstract_argument_type -val rawwit_tactic0 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type -val globwit_tactic0 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type -val wit_tactic0 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type +val rawwit_tactic0 : (raw_tactic_expr,rlevel) abstract_argument_type +val globwit_tactic0 : (glob_tactic_expr,glevel) abstract_argument_type +val wit_tactic0 : (glob_tactic_expr,tlevel) abstract_argument_type -val rawwit_tactic1 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type -val globwit_tactic1 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type -val wit_tactic1 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type +val rawwit_tactic1 : (raw_tactic_expr,rlevel) abstract_argument_type +val globwit_tactic1 : (glob_tactic_expr,glevel) abstract_argument_type +val wit_tactic1 : (glob_tactic_expr,tlevel) abstract_argument_type -val rawwit_tactic2 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type -val globwit_tactic2 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type -val wit_tactic2 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type +val rawwit_tactic2 : (raw_tactic_expr,rlevel) abstract_argument_type +val globwit_tactic2 : (glob_tactic_expr,glevel) abstract_argument_type +val wit_tactic2 : (glob_tactic_expr,tlevel) abstract_argument_type -val rawwit_tactic3 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type -val globwit_tactic3 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type -val wit_tactic3 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type +val rawwit_tactic3 : (raw_tactic_expr,rlevel) abstract_argument_type +val globwit_tactic3 : (glob_tactic_expr,glevel) abstract_argument_type +val wit_tactic3 : (glob_tactic_expr,tlevel) abstract_argument_type -val rawwit_tactic4 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type -val globwit_tactic4 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type -val wit_tactic4 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type +val rawwit_tactic4 : (raw_tactic_expr,rlevel) abstract_argument_type +val globwit_tactic4 : (glob_tactic_expr,glevel) abstract_argument_type +val wit_tactic4 : (glob_tactic_expr,tlevel) abstract_argument_type -val rawwit_tactic5 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type -val globwit_tactic5 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type -val wit_tactic5 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type +val rawwit_tactic5 : (raw_tactic_expr,rlevel) abstract_argument_type +val globwit_tactic5 : (glob_tactic_expr,glevel) abstract_argument_type +val wit_tactic5 : (glob_tactic_expr,tlevel) abstract_argument_type val is_tactic_genarg : argument_type -> bool @@ -132,6 +133,8 @@ module Prim : val ident : identifier Gram.Entry.e val name : name located Gram.Entry.e val identref : identifier located Gram.Entry.e + val pattern_ident : identifier Gram.Entry.e + val pattern_identref : identifier located Gram.Entry.e val base_ident : identifier Gram.Entry.e val natural : int Gram.Entry.e val bigint : Bigint.bigint Gram.Entry.e @@ -159,8 +162,12 @@ module Constr : val annot : constr_expr Gram.Entry.e val constr_pattern : constr_expr Gram.Entry.e val lconstr_pattern : constr_expr Gram.Entry.e - val binder : (name located list * constr_expr) Gram.Entry.e - val binder_let : local_binder Gram.Entry.e + val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e + val binder_let : local_binder list Gram.Entry.e + val binders_let : local_binder list Gram.Entry.e + val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e + val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e + val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e end module Module : @@ -176,7 +183,7 @@ module Tactic : val casted_open_constr : open_constr_expr Gram.Entry.e val constr_with_bindings : constr_expr with_bindings Gram.Entry.e val bindings : constr_expr bindings Gram.Entry.e - val constr_may_eval : (constr_expr,reference) may_eval Gram.Entry.e + val constr_may_eval : (constr_expr,reference or_by_notation) may_eval Gram.Entry.e val quantified_hypothesis : quantified_hypothesis Gram.Entry.e val int_or_var : int or_var Gram.Entry.e val red_expr : raw_red_expr Gram.Entry.e @@ -215,8 +222,16 @@ val symbol_of_production : Gramext.g_assoc option -> constr_entry -> (* Registering/resetting the level of an entry *) val find_position : - bool -> bool -> Gramext.g_assoc option -> int option -> - Gramext.position option * Gramext.g_assoc option * string option + bool (* true if for creation in pattern entry; false if in constr entry *) -> + Gramext.g_assoc option -> int option -> + Gramext.position option * Gramext.g_assoc option * string option * + (* for reinitialization: *) Gramext.g_assoc option + +val synchronize_level_positions : unit -> unit + +val register_empty_levels : bool -> Compat.token Gramext.g_symbol list -> + (Gramext.position option * Gramext.g_assoc option * + string option * Gramext.g_assoc option) list val remove_levels : int -> unit |