diff options
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 451 |
1 files changed, 249 insertions, 202 deletions
diff --git a/API/API.mli b/API/API.mli index 6c9ac98ffe..e46bca85fc 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1293,60 +1293,6 @@ sig type to_patch_substituted end -module Decl_kinds : -sig - type polymorphic = bool - type cumulative_inductive_flag = bool - type recursivity_kind = - | Finite - | CoFinite - | BiFinite - - type locality = - | Discharge - | Local - | Global - - type definition_object_kind = - | Definition - | Coercion - | SubClass - | CanonicalStructure - | Example - | Fixpoint - | CoFixpoint - | Scheme - | StructureComponent - | IdentityCoercion - | Instance - | Method - type theorem_kind = - | Theorem - | Lemma - | Fact - | Remark - | Property - | Proposition - | Corollary - type goal_object_kind = - | DefinitionBody of definition_object_kind - | Proof of theorem_kind - type goal_kind = locality * polymorphic * goal_object_kind - type assumption_object_kind = - | Definitional - | Logical - | Conjectural - type logical_kind = - | IsAssumption of assumption_object_kind - | IsDefinition of definition_object_kind - | IsProof of theorem_kind - type binding_kind = - | Explicit - | Implicit - type private_flag = bool - type definition_kind = locality * polymorphic * definition_object_kind -end - module Retroknowledge : sig type action @@ -1496,10 +1442,15 @@ sig type record_body = (Id.t * Constant.t array * projection_body array) option + type recursivity_kind = + | Finite + | CoFinite + | BiFinite + type mutual_inductive_body = { mind_packets : one_inductive_body array; mind_record : record_body option; - mind_finite : Decl_kinds.recursivity_kind; + mind_finite : recursivity_kind; mind_ntypes : int; mind_hyps : Context.Named.t; mind_nparams : int; @@ -1573,7 +1524,7 @@ sig (** Some (Some id): primitive record with id the binder name of the record in projections. Some None: non-primitive record *) - mind_entry_finite : Decl_kinds.recursivity_kind; + mind_entry_finite : Declarations.recursivity_kind; mind_entry_params : (Id.t * local_entry) list; mind_entry_inds : one_inductive_entry list; mind_entry_universes : inductive_universes; @@ -1856,6 +1807,60 @@ end (* Modules from intf/ *) (************************************************************************) +module Libnames : +sig + + open Util + open Names + + type full_path + val pr_path : full_path -> Pp.t + val make_path : Names.DirPath.t -> Names.Id.t -> full_path + val eq_full_path : full_path -> full_path -> bool + val repr_path : full_path -> Names.DirPath.t * Names.Id.t + val dirpath : full_path -> Names.DirPath.t + val path_of_string : string -> full_path + + type qualid + val make_qualid : Names.DirPath.t -> Names.Id.t -> qualid + val qualid_eq : qualid -> qualid -> bool + val repr_qualid : qualid -> Names.DirPath.t * Names.Id.t + val pr_qualid : qualid -> Pp.t + val string_of_qualid : qualid -> string + val qualid_of_string : string -> qualid + val qualid_of_path : full_path -> qualid + val qualid_of_dirpath : Names.DirPath.t -> qualid + val qualid_of_ident : Names.Id.t -> qualid + + type reference = + | Qualid of qualid Loc.located + | Ident of Names.Id.t Loc.located + val loc_of_reference : reference -> Loc.t option + val qualid_of_reference : reference -> qualid Loc.located + val pr_reference : reference -> Pp.t + + val is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool + val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t + val dirpath_of_string : string -> Names.DirPath.t + val pr_dirpath : Names.DirPath.t -> Pp.t + [@@ocaml.deprecated "Alias for DirPath.print"] + + val string_of_path : full_path -> string + + val basename : full_path -> Names.Id.t + + type object_name = full_path * Names.KerName.t + type object_prefix = { + obj_dir : DirPath.t; + obj_mp : ModPath.t; + obj_sec : DirPath.t; + } + + module Dirset : Set.S with type elt = DirPath.t + module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset + module Spmap : CSig.MapS with type key = full_path +end + module Misctypes : sig type evars_flag = bool @@ -1878,10 +1883,15 @@ sig | GSet (** representation of [Set] literal *) | GType of 'a (** representation of [Type] literal *) - type level_info = Names.Name.t Loc.located option + type 'a universe_kind = + | UAnonymous + | UUnknown + | UNamed of 'a + + type level_info = Libnames.reference universe_kind type glob_level = level_info glob_sort_gen - type sort_info = Names.Name.t Loc.located list + type sort_info = (Libnames.reference * int) option list type glob_sort = sort_info glob_sort_gen type ('a, 'b) gen_universe_decl = { @@ -1993,7 +2003,7 @@ end module Univops : sig - val universes_of_constr : Constr.constr -> Univ.LSet.t + val universes_of_constr : Environ.env -> Constr.constr -> Univ.LSet.t val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t end @@ -2034,56 +2044,6 @@ sig [@@ocaml.deprecated "alias of API.Names"] end -module Libnames : -sig - - open Util - open Names - - type full_path - val pr_path : full_path -> Pp.t - val make_path : Names.DirPath.t -> Names.Id.t -> full_path - val eq_full_path : full_path -> full_path -> bool - val repr_path : full_path -> Names.DirPath.t * Names.Id.t - val dirpath : full_path -> Names.DirPath.t - val path_of_string : string -> full_path - - type qualid - val make_qualid : Names.DirPath.t -> Names.Id.t -> qualid - val qualid_eq : qualid -> qualid -> bool - val repr_qualid : qualid -> Names.DirPath.t * Names.Id.t - val pr_qualid : qualid -> Pp.t - val string_of_qualid : qualid -> string - val qualid_of_string : string -> qualid - val qualid_of_path : full_path -> qualid - val qualid_of_dirpath : Names.DirPath.t -> qualid - val qualid_of_ident : Names.Id.t -> qualid - - type reference = - | Qualid of qualid Loc.located - | Ident of Names.Id.t Loc.located - val loc_of_reference : reference -> Loc.t option - val qualid_of_reference : reference -> qualid Loc.located - val pr_reference : reference -> Pp.t - - val is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool - val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t - val dirpath_of_string : string -> Names.DirPath.t - val pr_dirpath : Names.DirPath.t -> Pp.t - [@@ocaml.deprecated "Alias for DirPath.print"] - - val string_of_path : full_path -> string - - val basename : full_path -> Names.Id.t - - type object_name = full_path * Names.KerName.t - type object_prefix = Names.DirPath.t * (Names.ModPath.t * Names.DirPath.t) - - module Dirset : Set.S with type elt = DirPath.t - module Dirmap : Map.ExtS with type key = DirPath.t and module Set := Dirset - module Spmap : CSig.MapS with type key = full_path -end - module Globnames : sig @@ -2196,6 +2156,66 @@ sig | SubEvar of Evar.t end +module Decl_kinds : +sig + type polymorphic = bool + type cumulative_inductive_flag = bool + type recursivity_kind = Declarations.recursivity_kind = + | Finite + | CoFinite + | BiFinite + [@@ocaml.deprecated "Please use [Declarations.recursivity_kind"] + + type discharge = + | DoDischarge + | NoDischarge + + type locality = + | Discharge + | Local + | Global + + type definition_object_kind = + | Definition + | Coercion + | SubClass + | CanonicalStructure + | Example + | Fixpoint + | CoFixpoint + | Scheme + | StructureComponent + | IdentityCoercion + | Instance + | Method + | Let + type theorem_kind = + | Theorem + | Lemma + | Fact + | Remark + | Property + | Proposition + | Corollary + type goal_object_kind = + | DefinitionBody of definition_object_kind + | Proof of theorem_kind + type goal_kind = locality * polymorphic * goal_object_kind + type assumption_object_kind = + | Definitional + | Logical + | Conjectural + type logical_kind = + | IsAssumption of assumption_object_kind + | IsDefinition of definition_object_kind + | IsProof of theorem_kind + type binding_kind = + | Explicit + | Implicit + type private_flag = bool + type definition_kind = locality * polymorphic * definition_object_kind +end + module Glob_term : sig type 'a cases_pattern_r = @@ -2374,7 +2394,7 @@ sig and case_expr = constr_expr * Names.Name.t Loc.located option * cases_pattern_expr option and branch_expr = - (cases_pattern_expr list Loc.located list * constr_expr) Loc.located + (cases_pattern_expr list list * constr_expr) Loc.located and binder_expr = Names.Name.t Loc.located list * binder_kind * constr_expr @@ -2745,10 +2765,10 @@ sig type universe_binders type universe_opt_subst val fresh_inductive_instance : Environ.env -> Names.inductive -> Constr.pinductive Univ.in_universe_context_set - val new_Type : Names.DirPath.t -> Constr.types + val new_Type : unit -> Constr.types val type_of_global : Globnames.global_reference -> Constr.types Univ.in_universe_context_set val constr_of_global : Globnames.global_reference -> Constr.t - val new_univ_level : Names.DirPath.t -> Univ.Level.t + val new_univ_level : unit -> Univ.Level.t val new_sort_in_family : Sorts.family -> Sorts.t val pr_with_global_universes : Univ.Level.t -> Pp.t val pr_universe_opt_subst : universe_opt_subst -> Pp.t @@ -2761,6 +2781,8 @@ sig end type universe_constraints = Constraints.t + [@@ocaml.deprecated "Use Constraints.t"] + end module UState : @@ -3097,7 +3119,7 @@ sig val fold : Evd.evar_map -> ('a -> constr -> 'a) -> 'a -> constr -> 'a val existential_type : Evd.evar_map -> existential -> types val iter : Evd.evar_map -> (constr -> unit) -> constr -> unit - val eq_constr_universes : Evd.evar_map -> constr -> constr -> Universes.universe_constraints option + val eq_constr_universes : Evd.evar_map -> constr -> constr -> Universes.Constraints.t option val eq_constr_nounivs : Evd.evar_map -> constr -> constr -> bool val compare_constr : Evd.evar_map -> (constr -> constr -> bool) -> constr -> constr -> bool val isApp : Evd.evar_map -> constr -> bool @@ -3712,7 +3734,7 @@ end module Retyping : (* reconstruct the type of a term knowing that it was already typechecked *) sig val get_type_of : ?polyprop:bool -> ?lax:bool -> Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.types - val get_sort_family_of : ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.family + val get_sort_family_of : ?truncation_style:bool -> ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.family val expand_projection : Environ.env -> Evd.evar_map -> Names.Projection.t -> EConstr.constr -> EConstr.constr list -> EConstr.constr val get_sort_of : ?polyprop:bool -> Environ.env -> Evd.evar_map -> EConstr.types -> Sorts.t @@ -3831,10 +3853,9 @@ sig type matching_result = { m_sub : bound_ident_map * Ltac_pretype.patvar_map; m_ctx : EConstr.constr } - val match_subterm_gen : Environ.env -> Evd.evar_map -> - bool -> - binding_bound_vars * Pattern.constr_pattern -> EConstr.constr -> - matching_result IStream.t + val match_subterm : Environ.env -> Evd.evar_map -> + binding_bound_vars * Pattern.constr_pattern -> EConstr.constr -> + matching_result IStream.t val matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Ltac_pretype.patvar_map end @@ -3985,7 +4006,7 @@ sig type instance_flag = bool option type coercion_flag = bool - type inductive_flag = Decl_kinds.recursivity_kind + type inductive_flag = Declarations.recursivity_kind type lname = Names.Name.t Loc.located type lident = Names.Id.t Loc.located type opacity_flag = @@ -4028,8 +4049,6 @@ sig type verbose_flag = bool - type obsolete_locality = bool - type universe_decl_expr = (lident list, Misctypes.glob_constraint list) gen_universe_decl type ident_decl = lident * universe_decl_expr option @@ -4140,33 +4159,27 @@ sig type vernac_expr = | VernacLoad of verbose_flag * string - | VernacTime of vernac_expr Loc.located - | VernacRedirect of string * vernac_expr Loc.located - | VernacTimeout of int * vernac_expr - | VernacFail of vernac_expr - | VernacSyntaxExtension of - bool * obsolete_locality * (lstring * syntax_modifier list) - | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) + | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) + | VernacOpenCloseScope of bool * scope_name | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * class_rawexpr list - | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) * + | VernacInfix of (lstring * syntax_modifier list) * Constrexpr.constr_expr * scope_name option | VernacNotation of - obsolete_locality * Constrexpr.constr_expr * (lstring * syntax_modifier list) * + Constrexpr.constr_expr * (lstring * syntax_modifier list) * scope_name option | VernacNotationAddFormat of string * string * string - | VernacDefinition of - (Decl_kinds.locality option * Decl_kinds.definition_object_kind) * ident_decl * definition_expr + | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * ident_decl * definition_expr | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of Constrexpr.constr_expr - | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) * + | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * inline * (ident_decl list * Constrexpr.constr_expr) with_coercion list | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of - Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list + Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of - Decl_kinds.locality option * (cofixpoint_expr * decl_notation list) list + Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list @@ -4177,9 +4190,9 @@ sig Libnames.reference option * bool option * Libnames.reference list | VernacImport of bool * Libnames.reference list | VernacCanonical of Libnames.reference Misctypes.or_by_notation - | VernacCoercion of obsolete_locality * Libnames.reference Misctypes.or_by_notation * + | VernacCoercion of Libnames.reference Misctypes.or_by_notation * class_rawexpr * class_rawexpr - | VernacIdentityCoercion of obsolete_locality * lident * + | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr | VernacNameSectionHypSet of lident * section_subset_expr | VernacInstance of @@ -4213,9 +4226,9 @@ sig | VernacBackTo of int | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * Libnames.reference list - | VernacHints of obsolete_locality * string list * hints_expr + | VernacHints of string list * hints_expr | VernacSyntacticDefinition of Names.Id.t Loc.located * (Names.Id.t list * Constrexpr.constr_expr) * - obsolete_locality * onlyparsing_flag + onlyparsing_flag | VernacDeclareImplicits of Libnames.reference Misctypes.or_by_notation * (Constrexpr.explicitation * bool * bool) list list | VernacArguments of Libnames.reference Misctypes.or_by_notation * @@ -4277,6 +4290,16 @@ sig and vernac_classification = vernac_type * vernac_when and one_inductive_expr = ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list + +type vernac_control = + | VernacExpr of vernac_expr + (* Control *) + | VernacTime of vernac_control Loc.located + | VernacRedirect of string * vernac_control Loc.located + | VernacTimeout of int * vernac_control + | VernacFail of vernac_control + + end (* XXX: end of moved from intf *) @@ -4329,6 +4352,7 @@ sig | Later : [ `thunk ] delay val print_universes : bool ref val print_evar_arguments : bool ref + val print_allow_match_default_clause : bool ref val detype : 'a delay -> ?lax:bool -> bool -> Names.Id.Set.t -> Environ.env -> Evd.evar_map -> EConstr.constr -> 'a Glob_term.glob_constr_g val subst_glob_constr : Mod_subst.substitution -> Glob_term.glob_constr -> Glob_term.glob_constr val set_detype_anonymous : (?loc:Loc.t -> int -> Names.Id.t) -> unit @@ -4602,6 +4626,9 @@ end module Constrintern : sig + + open Evd + type ltac_sign = { ltac_vars : Names.Id.Set.t; ltac_bound : Names.Id.Set.t; @@ -4617,11 +4644,11 @@ sig | Variable type internalization_env = var_internalization_data Names.Id.Map.t - val interp_constr_evars : Environ.env -> Evd.evar_map ref -> - ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.constr + val interp_constr_evars : Environ.env -> evar_map -> + ?impls:internalization_env -> Constrexpr.constr_expr -> evar_map * EConstr.constr - val interp_type_evars : Environ.env -> Evd.evar_map ref -> - ?impls:internalization_env -> Constrexpr.constr_expr -> EConstr.types + val interp_type_evars : Environ.env -> Evd.evar_map -> + ?impls:internalization_env -> Constrexpr.constr_expr -> evar_map * EConstr.types val empty_ltac_sign : ltac_sign val intern_gen : Pretyping.typing_constraint -> Environ.env -> @@ -4639,10 +4666,12 @@ sig val locate_reference : Libnames.qualid -> Globnames.global_reference val interp_type : Environ.env -> Evd.evar_map -> ?impls:internalization_env -> Constrexpr.constr_expr -> Constr.types Evd.in_evar_universe_context + val interp_context_evars : ?global_level:bool -> ?impl_env:internalization_env -> ?shift:int -> - Environ.env -> Evd.evar_map ref -> Constrexpr.local_binder_expr list -> - internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits) + Environ.env -> Evd.evar_map -> Constrexpr.local_binder_expr list -> + evar_map * (internalization_env * ((Environ.env * EConstr.rel_context) * Impargs.manual_implicits)) + val compute_internalization_data : Environ.env -> var_internalization_type -> Constr.types -> Impargs.manual_explicitation list -> var_internalization_data val empty_internalization_env : internalization_env @@ -4783,7 +4812,7 @@ sig | IntroNeedsProduct | DoesNotOccurIn of Constr.t * Names.Id.t | NoSuchHyp of Names.Id.t - exception RefinerError of refiner_error + exception RefinerError of Environ.env * Evd.evar_map * refiner_error val catchable_exception : exn -> bool end @@ -4795,24 +4824,26 @@ end module Proof : sig - type proof - type 'a focus_kind + type t + type proof = t + [@@ocaml.deprecated "please use [Proof.t]"] - val proof : proof -> + type 'a focus_kind + val proof : t -> Goal.goal list * (Goal.goal list * Goal.goal list) list * Goal.goal list * Goal.goal list * Evd.evar_map val run_tactic : Environ.env -> - unit Proofview.tactic -> proof -> proof * (bool * Proofview_monad.Info.tree) - val unshelve : proof -> proof - val maximal_unfocus : 'a focus_kind -> proof -> proof - val pr_proof : proof -> Pp.t + unit Proofview.tactic -> t -> t * (bool * Proofview_monad.Info.tree) + val unshelve : t -> t + val maximal_unfocus : 'a focus_kind -> t -> t + val pr_proof : t -> Pp.t module V82 : sig - val grab_evars : proof -> proof + val grab_evars : t -> t - val subgoals : proof -> Goal.goal list Evd.sigma + val subgoals : t -> Goal.goal list Evd.sigma [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] end @@ -4826,24 +4857,25 @@ end module Proof_global : sig - type state + type t + type state = t + [@@ocaml.deprecated "please use [Proof_global.t]"] type proof_mode = { name : string; set : unit -> unit ; reset : unit -> unit } - type proof_universes = UState.t * Universes.universe_binders option type proof_object = { id : Names.Id.t; entries : Safe_typing.private_constants Entries.definition_entry list; persistence : Decl_kinds.goal_kind; - universes: proof_universes; + universes: UState.t; } type proof_ending = | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * - proof_universes + UState.t | Proved of Vernacexpr.opacity_flag * Vernacexpr.lident option * proof_object @@ -4857,14 +4889,14 @@ sig Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> Proofview.telescope -> proof_terminator -> unit val with_current_proof : - (unit Proofview.tactic -> Proof.proof -> Proof.proof * 'a) -> 'a + (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a val simple_with_current_proof : - (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit + (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit val compact_the_proof : unit -> unit val register_proof_mode : proof_mode -> unit exception NoCurrentProof - val give_me_the_proof : unit -> Proof.proof + val give_me_the_proof : unit -> Proof.t (** @raise NoCurrentProof when outside proof mode. *) val discard_all : unit -> unit @@ -4951,8 +4983,6 @@ sig val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool - val pf_is_matching : Goal.goal Evd.sigma -> Pattern.constr_pattern -> EConstr.constr -> bool - val pf_hyps_types : Goal.goal Evd.sigma -> (Names.Id.t * EConstr.types) list val pr_gls : Goal.goal Evd.sigma -> Pp.t @@ -4995,9 +5025,9 @@ sig val by : unit Proofview.tactic -> bool val solve : ?with_end_tac:unit Proofview.tactic -> Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> - Proof.proof -> Proof.proof * bool + Proof.t -> Proof.t * bool val cook_proof : - unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind)) + unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * UState.t * Decl_kinds.goal_kind)) val get_current_context : unit -> Evd.evar_map * Environ.env val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types @@ -5151,9 +5181,7 @@ sig val gallina_ext : vernac_expr Gram.entry val command : vernac_expr Gram.entry val syntax : vernac_expr Gram.entry - val vernac : vernac_expr Gram.entry val rec_definition : (fixpoint_expr * decl_notation list) Gram.entry - val vernac_eoi : vernac_expr Gram.entry val noedit_mode : vernac_expr Gram.entry val command_entry : vernac_expr Gram.entry val red_expr : raw_red_expr Gram.entry @@ -5234,16 +5262,20 @@ end module Genprint : sig - type printer_with_level = + type 'a with_level = { default_already_surrounded : Notation_term.tolerability; default_ensure_surrounded : Notation_term.tolerability; - printer : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t } + printer : 'a } type printer_result = - | PrinterBasic of (unit -> Pp.t) - | PrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) - | PrinterNeedsContextAndLevel of printer_with_level - type 'a printer = 'a -> Pp.t - type 'a top_printer = 'a -> printer_result +| PrinterBasic of (unit -> Pp.t) +| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level + type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t + type top_printer_result = + | TopPrinterBasic of (unit -> Pp.t) + | TopPrinterNeedsContext of (Environ.env -> Evd.evar_map -> Pp.t) + | TopPrinterNeedsContextAndLevel of printer_fun_with_level with_level + type 'a printer = 'a -> printer_result + type 'a top_printer = 'a -> top_printer_result val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw printer -> 'glb printer -> 'top top_printer -> unit val register_vernac_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> @@ -5945,7 +5977,7 @@ end module Ppvernac : sig - val pr_vernac : Vernacexpr.vernac_expr -> Pp.t + val pr_vernac : Vernacexpr.vernac_control -> Pp.t val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t end @@ -6022,21 +6054,53 @@ sig val show_term : Names.Id.t option -> Pp.t end -module Command : +module ComDefinition : sig + val do_definition : + program_mode:bool -> + Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option -> + Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> + Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit +end + +module ComFixpoint : +sig + open Names open Constrexpr - open Vernacexpr type structured_fixpoint_expr = { fix_name : Id.t; - fix_univs : universe_decl_expr option; + fix_univs : Vernacexpr.universe_decl_expr option; fix_annot : Id.t Loc.located option; fix_binders : local_binder_expr list; fix_body : constr_expr option; fix_type : constr_expr } + type recursive_preentry = Names.Id.t list * Constr.t option list * Constr.types list + + val interp_fixpoint : + cofix:bool -> + structured_fixpoint_expr list -> Vernacexpr.decl_notation list -> + recursive_preentry * Univdecls.universe_decl * UState.t * + (EConstr.rel_context * Impargs.manual_implicits * int option) list + + val extract_fixpoint_components : bool -> + (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> + structured_fixpoint_expr list * Vernacexpr.decl_notation list + + val do_fixpoint : + Decl_kinds.locality -> Decl_kinds.polymorphic -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit + +end + +module ComInductive : +sig + open Names + open Constrexpr + open Vernacexpr + type structured_one_inductive_expr = { ind_name : Id.t; ind_univs : universe_decl_expr option; @@ -6047,29 +6111,11 @@ sig type structured_inductive_expr = local_binder_expr list * structured_one_inductive_expr list - type recursive_preentry = Names.Id.t list * Constr.t option list * Constr.types list - type one_inductive_impls val do_mutual_inductive : (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> - Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit - - val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.universe_decl_expr option -> - Constrexpr.local_binder_expr list -> Redexpr.red_expr option -> Constrexpr.constr_expr -> - Constrexpr.constr_expr option -> unit Lemmas.declaration_hook -> unit - - val do_fixpoint : - Decl_kinds.locality -> Decl_kinds.polymorphic -> (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> unit - - val extract_fixpoint_components : bool -> - (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list -> - structured_fixpoint_expr list * Vernacexpr.decl_notation list - - val interp_fixpoint : - structured_fixpoint_expr list -> Vernacexpr.decl_notation list -> - recursive_preentry * Univdecls.universe_decl * UState.t * - (EConstr.rel_context * Impargs.manual_implicits * int option) list + Decl_kinds.private_flag -> Declarations.recursivity_kind -> unit val extract_mutual_inductive_declaration_components : (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> @@ -6079,7 +6125,7 @@ sig structured_inductive_expr -> Vernacexpr.decl_notation list -> Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic -> - Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> + Decl_kinds.private_flag -> Declarations.recursivity_kind -> Entries.mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list val declare_mutual_inductive_with_eliminations : @@ -6094,6 +6140,7 @@ sig ?abstract:bool -> ?global:bool -> ?refine:bool -> + program_mode:bool -> Decl_kinds.polymorphic -> Constrexpr.local_binder_expr list -> Vernacexpr.typeclass_constraint -> @@ -6108,9 +6155,9 @@ end module Vernacstate : sig - type t = { (* TODO: inline records in OCaml 4.03 *) + type t = { system : States.state; (* summary + libstack *) - proof : Proof_global.state; (* proof state *) + proof : Proof_global.t; (* proof state *) shallow : bool (* is the state trimmed down (libstack) *) } @@ -6178,7 +6225,7 @@ sig val classify_as_proofstep : Vernacexpr.vernac_classification val classify_as_query : Vernacexpr.vernac_classification val classify_as_sideeff : Vernacexpr.vernac_classification - val classify_vernac : Vernacexpr.vernac_expr -> Vernacexpr.vernac_classification + val classify_vernac : Vernacexpr.vernac_control -> Vernacexpr.vernac_classification end module Stm : |