diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.ml | 22 | ||||
| -rw-r--r-- | API/API.mli | 808 |
2 files changed, 484 insertions, 346 deletions
diff --git a/API/API.ml b/API/API.ml index c952e123d4..6e61063e4b 100644 --- a/API/API.ml +++ b/API/API.ml @@ -10,9 +10,9 @@ To see such order issue the comand: -``` -bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done && echo -e "\n## highparsing files" && cat parsing/highparsing.mllib' > API/link -``` + ``` + bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done > API/link + ``` *) (******************************************************************************) @@ -43,7 +43,7 @@ module Cbytecodes = Cbytecodes (* module Copcodes *) module Cemitcodes = Cemitcodes (* module Nativevalues *) -(* module Primitives *) +(* module CPrimitives *) module Opaqueproof = Opaqueproof module Declareops = Declareops module Retroknowledge = Retroknowledge @@ -131,6 +131,7 @@ module Geninterp = Geninterp (******************************************************************************) (* Pretyping *) (******************************************************************************) +module Ltac_pretype = Ltac_pretype module Locusops = Locusops module Pretype_errors = Pretype_errors module Reductionops = Reductionops @@ -162,6 +163,7 @@ module Indrec = Indrec (* module Cases *) module Pretyping = Pretyping module Unification = Unification +module Univdecls = Univdecls (******************************************************************************) (* interp *) (******************************************************************************) @@ -169,7 +171,6 @@ module Stdarg = Stdarg module Genintern = Genintern module Constrexpr_ops = Constrexpr_ops module Notation_ops = Notation_ops -module Ppextend = Ppextend module Notation = Notation module Dumpglob = Dumpglob (* module Syntax_def *) @@ -212,7 +213,7 @@ module Pputils = Pputils module Ppconstr = Ppconstr module Printer = Printer (* module Printmod *) -(* module Prettyp *) +module Prettyp = Prettyp module Ppvernac = Ppvernac (******************************************************************************) @@ -224,6 +225,9 @@ module Pcoq = Pcoq module Egramml = Egramml (* Egramcoq *) +module G_vernac = G_vernac +module G_proofs = G_proofs + (******************************************************************************) (* Tactics *) (******************************************************************************) @@ -277,9 +281,3 @@ module Vernacentries = Vernacentries (******************************************************************************) module Vernac_classifier = Vernac_classifier module Stm = Stm - -(******************************************************************************) -(* Highparsing *) -(******************************************************************************) -module G_vernac = G_vernac -module G_proofs = G_proofs diff --git a/API/API.mli b/API/API.mli index bb24d5768f..e207930771 100644 --- a/API/API.mli +++ b/API/API.mli @@ -10,7 +10,7 @@ in Coq. To see such order issue the comand: ``` - bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done && echo -e "\n## highparsing files" && cat parsing/highparsing.mllib' > API/link + bash -c 'for i in kernel intf library engine pretyping interp proofs parsing printing tactics vernac stm toplevel; do echo -e "\n## $i files" && cat ${i}/${i}.mllib; done > API/link ``` Note however that files in intf/ are located manually now as their @@ -47,7 +47,7 @@ sig val of_string : string -> t val of_string_soft : string -> t val to_string : t -> string - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t module Set : Set.S with type elt = t module Map : Map.ExtS with type key = t and module Set := Set @@ -67,7 +67,7 @@ sig val equal : t -> t -> bool val hash : t -> int val hcons : t -> t - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t end type name = Name.t = @@ -128,7 +128,7 @@ sig val compare : t -> t -> int val label : t -> Label.t val repr : t -> ModPath.t * DirPath.t * Label.t - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t val to_string : t -> string end @@ -159,7 +159,7 @@ sig val modpath : t -> ModPath.t val label : t -> Label.t val user : t -> KerName.t - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t end module Projection : @@ -169,6 +169,8 @@ sig val map : (Constant.t -> Constant.t) -> t -> t val constant : t -> Constant.t val equal : t -> t -> bool + val unfolded : t -> bool + val unfold : t -> t end type evaluable_global_reference = @@ -212,7 +214,7 @@ sig val var_full_transparent_state : transparent_state val cst_full_transparent_state : transparent_state - val pr_kn : KerName.t -> Pp.std_ppcmds + val pr_kn : KerName.t -> Pp.t [@@ocaml.deprecated "alias of API.Names.KerName.print"] val eq_constant : Constant.t -> Constant.t -> bool @@ -297,11 +299,11 @@ sig val make_con : ModPath.t -> DirPath.t -> Label.t -> Constant.t [@@ocaml.deprecated "alias of API.Names.Constant.make3"] - val debug_pr_con : Constant.t -> Pp.std_ppcmds + val debug_pr_con : Constant.t -> Pp.t - val debug_pr_mind : MutInd.t -> Pp.std_ppcmds + val debug_pr_mind : MutInd.t -> Pp.t - val pr_con : Constant.t -> Pp.std_ppcmds + val pr_con : Constant.t -> Pp.t val string_of_con : Constant.t -> string @@ -323,7 +325,7 @@ sig sig type t val set : t - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t end type universe_level = Level.t @@ -331,13 +333,13 @@ sig module LSet : sig include CSig.SetS with type elt = universe_level - val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.t) -> t -> Pp.t end module Universe : sig type t - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t end type universe = Universe.t @@ -348,7 +350,7 @@ sig val empty : t val of_array : Level.t array -> t val to_array : t -> Level.t array - val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.t) -> t -> Pp.t end type 'a puniverses = 'a * Instance.t @@ -418,7 +420,7 @@ sig val union : 'a t -> 'a t -> 'a t val diff : 'a t -> 'a t -> 'a t val subst_union : 'a option t -> 'a option t -> 'a option t - val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + val pr : ('a -> Pp.t) -> 'a t -> Pp.t end type 'a universe_map = 'a LMap.t @@ -426,18 +428,18 @@ sig type universe_level_subst = universe_level universe_map val enforce_leq : Universe.t constraint_function - val pr_uni : Universe.t -> Pp.std_ppcmds - val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> UContext.t -> Pp.std_ppcmds - val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> ContextSet.t -> Pp.std_ppcmds - val pr_universe_subst : universe_subst -> Pp.std_ppcmds - val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds - val pr_constraints : (Level.t -> Pp.std_ppcmds) -> Constraint.t -> Pp.std_ppcmds + val pr_uni : Universe.t -> Pp.t + val pr_universe_context : (Level.t -> Pp.t) -> UContext.t -> Pp.t + val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t + val pr_universe_subst : universe_subst -> Pp.t + val pr_universe_level_subst : universe_level_subst -> Pp.t + val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t end module UGraph : sig type t - val pr_universes : (Univ.Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr_universes : (Univ.Level.t -> Pp.t) -> t -> Pp.t end module Esubst : @@ -1033,8 +1035,8 @@ sig val subst_mps : substitution -> Constr.t -> Constr.t val subst_constant : substitution -> Names.Constant.t -> Names.Constant.t val subst_ind : substitution -> Names.inductive -> Names.inductive - val debug_pr_subst : substitution -> Pp.std_ppcmds - val debug_pr_delta : delta_resolver -> Pp.std_ppcmds + val debug_pr_subst : substitution -> Pp.t + val debug_pr_delta : delta_resolver -> Pp.t end module Opaqueproof : @@ -1185,8 +1187,6 @@ sig | RegularArity of 'a | TemplateArity of 'b - type constant_type = (Constr.types, Context.Rel.t * template_arity) declaration_arity - type constant_universes = | Monomorphic_const of Univ.universe_context | Polymorphic_const of Univ.abstract_universe_context @@ -1208,7 +1208,7 @@ sig type constant_body = { const_hyps : Context.Named.t; const_body : constant_def; - const_type : constant_type; + const_type : Term.types; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : constant_universes; const_proj : projection_body option; @@ -1280,23 +1280,28 @@ sig | Algebraic of module_expression | Struct of module_signature | FullStruct - and module_body = + and 'a generic_module_body = { mod_mp : Names.ModPath.t; - mod_expr : module_implementation; + mod_expr : 'a; mod_type : module_signature; mod_type_alg : module_expression option; mod_constraints : Univ.ContextSet.t; mod_delta : Mod_subst.delta_resolver; - mod_retroknowledge : Retroknowledge.action list + mod_retroknowledge : 'a module_retroknowledge; } and module_signature = (module_type_body,structure_body) functorize - and module_type_body = module_body + and module_body = module_implementation generic_module_body + and module_type_body = unit generic_module_body and structure_body = (Names.Label.t * structure_field_body) list and structure_field_body = | SFBconst of constant_body | SFBmind of mutual_inductive_body | SFBmodule of module_body | SFBmodtype of module_type_body + and _ module_retroknowledge = + | ModBodyRK : + Retroknowledge.action list -> module_implementation module_retroknowledge + | ModTypeRK : unit module_retroknowledge end module Declareops : @@ -1345,6 +1350,9 @@ sig type inline = int option type 'a proof_output = Constr.t Univ.in_universe_context_set * 'a type 'a const_entry_body = 'a proof_output Future.computation + type constant_universes_entry = + | Monomorphic_const_entry of Univ.universe_context + | Polymorphic_const_entry of Univ.universe_context type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) @@ -1352,8 +1360,7 @@ sig (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : Constr.types option; - const_entry_polymorphic : bool; - const_entry_universes : Univ.UContext.t; + const_entry_universes : constant_universes_entry; const_entry_opaque : bool; const_entry_inline_code : bool } type parameter_entry = Context.Named.t option * bool * Constr.types Univ.in_universe_context * inline @@ -1584,7 +1591,6 @@ end module Typeops : sig val infer_type : Environ.env -> Term.types -> Environ.unsafe_type_judgment - val type_of_constant_type : Environ.env -> Declarations.constant_type -> Term.types val type_of_constant_in : Environ.env -> Term.pconstant -> Term.types end @@ -1642,6 +1648,14 @@ sig type sort_info = Names.Name.t Loc.located list type glob_sort = sort_info glob_sort_gen + type ('a, 'b) gen_universe_decl = { + univdecl_instance : 'a; (* Declared universes *) + univdecl_extensible_instance : bool; (* Can new universes be added *) + univdecl_constraints : 'b; (* Declared constraints *) + univdecl_extensible_constraints : bool (* Can new constraints be added *) } + + type glob_constraint = glob_level * Univ.constraint_type * glob_level + type case_style = Term.case_style = | LetStyle | IfStyle @@ -1750,10 +1764,10 @@ module Nameops : sig val atompart_of_id : Names.Id.t -> string - val pr_id : Names.Id.t -> Pp.std_ppcmds + val pr_id : Names.Id.t -> Pp.t [@@ocaml.deprecated "alias of API.Names.Id.print"] - val pr_name : Names.Name.t -> Pp.std_ppcmds + val pr_name : Names.Name.t -> Pp.t [@@ocaml.deprecated "alias of API.Names.Name.print"] val name_fold : (Names.Id.t -> 'a -> 'a) -> Names.Name.t -> 'a -> 'a @@ -1762,7 +1776,7 @@ sig val increment_subscript : Names.Id.t -> Names.Id.t val make_ident : string -> int option -> Names.Id.t val out_name : Names.Name.t -> Names.Id.t - val pr_lab : Names.Label.t -> Pp.std_ppcmds + val pr_lab : Names.Label.t -> Pp.t module Name : sig include module type of struct include Names.Name end @@ -1778,9 +1792,10 @@ sig open Names type full_path - val pr_path : full_path -> Pp.std_ppcmds + 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 @@ -1788,7 +1803,7 @@ sig 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.std_ppcmds + 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 @@ -1800,12 +1815,12 @@ sig | 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.std_ppcmds + 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.std_ppcmds + val pr_dirpath : Names.DirPath.t -> Pp.t val string_of_path : full_path -> string val basename : full_path -> Names.Id.t @@ -1899,7 +1914,11 @@ module Summary : sig type frozen - type marshallable + + type marshallable = + [ `Yes (* Full data will be marshalled to disk *) + | `No (* Full data will be store in memory, e.g. for Undo *) + | `Shallow ] (* Only part of the data will be marshalled to a slave process *) type 'a summary_declaration = { freeze_function : marshallable -> 'a; @@ -1921,24 +1940,19 @@ module Nametab : sig exception GlobalizationError of Libnames.qualid - type ltac_constant = Names.KerName.t - val global : Libnames.reference -> Globnames.global_reference val global_of_path : Libnames.full_path -> Globnames.global_reference val shortest_qualid_of_global : Names.Id.Set.t -> Globnames.global_reference -> Libnames.qualid val path_of_global : Globnames.global_reference -> Libnames.full_path val locate_extended : Libnames.qualid -> Globnames.extended_global_reference val full_name_module : Libnames.qualid -> Names.DirPath.t - val locate_tactic : Libnames.qualid -> Names.KerName.t - val pr_global_env : Names.Id.Set.t -> Globnames.global_reference -> Pp.std_ppcmds - val shortest_qualid_of_tactic : Names.KerName.t -> Libnames.qualid + val pr_global_env : Names.Id.Set.t -> Globnames.global_reference -> Pp.t val basename_of_global : Globnames.global_reference -> Names.Id.t type visibility = | Until of int | Exactly of int - val push_tactic : visibility -> Libnames.full_path -> Names.KerName.t -> unit val error_global_not_found : ?loc:Loc.t -> Libnames.qualid -> 'a val shortest_qualid_of_module : Names.ModPath.t -> Libnames.qualid val dirpath_of_module : Names.ModPath.t -> Names.DirPath.t @@ -1946,6 +1960,40 @@ sig val dirpath_of_global : Globnames.global_reference -> Names.DirPath.t val locate : Libnames.qualid -> Globnames.global_reference val locate_constant : Libnames.qualid -> Names.Constant.t + + (** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *) + + module type UserName = sig + type t + val equal : t -> t -> bool + val to_string : t -> string + val repr : t -> Names.Id.t * Names.Id.t list + end + + module type EqualityType = + sig + type t + val equal : t -> t -> bool + end + + module type NAMETREE = sig + type elt + type t + type user_name + + val empty : t + val push : visibility -> user_name -> elt -> t -> t + val locate : Libnames.qualid -> t -> elt + val find : user_name -> t -> elt + val exists : user_name -> t -> bool + val user_name : Libnames.qualid -> t -> user_name + val shortest_qualid : Names.Id.Set.t -> user_name -> t -> Libnames.qualid + val find_prefixes : Libnames.qualid -> t -> elt list + end + + module Make (U : UserName) (E : EqualityType) : + NAMETREE with type user_name = U.t and type elt = E.t + end module Global : @@ -2016,7 +2064,8 @@ end module States : sig - val with_state_protection_on_exception : ('a -> 'b) -> 'a -> 'b + type state + val with_state_protection : ('a -> 'b) -> 'a -> 'b end @@ -2053,7 +2102,7 @@ sig type key val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option val declare_equiv_keys : key -> key -> unit - val pr_keys : (Globnames.global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds + val pr_keys : (Globnames.global_reference -> Pp.t) -> Pp.t end module Coqlib : @@ -2106,6 +2155,7 @@ sig val coq_not_ref : Globnames.global_reference lazy_t val coq_or_ref : Globnames.global_reference lazy_t val build_coq_and : Globnames.global_reference Util.delayed + val build_coq_or : Globnames.global_reference Util.delayed val build_coq_I : Globnames.global_reference Util.delayed val coq_reference : string -> string list -> string -> Globnames.global_reference end @@ -2128,14 +2178,14 @@ sig val constr_of_global : Globnames.global_reference -> Constr.t val new_univ_level : Names.DirPath.t -> Univ.Level.t val new_sort_in_family : Sorts.family -> Sorts.t - val pr_with_global_universes : Univ.Level.t -> Pp.std_ppcmds - val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds + val pr_with_global_universes : Univ.Level.t -> Pp.t + val pr_universe_opt_subst : universe_opt_subst -> Pp.t type universe_constraint module Constraints : sig type t - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t end type universe_constraints = Constraints.t @@ -2293,7 +2343,7 @@ sig val universe_context_set : evar_map -> Univ.ContextSet.t val evar_ident : evar -> evar_map -> Names.Id.t option val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list - val universe_context : ?names:(Names.Id.t Loc.located) list -> evar_map -> + val universe_context : names:(Names.Id.t Loc.located) list -> extensible:bool -> evar_map -> (Names.Id.t * Univ.Level.t) list * Univ.UContext.t val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map @@ -2454,7 +2504,6 @@ sig constr_expr list list * local_binder_expr list list - type typeclass_constraint = (Names.Name.t Loc.located * Names.Id.t Loc.located list option) * Decl_kinds.binding_kind * constr_expr type constr_pattern_expr = constr_expr end @@ -2708,13 +2757,6 @@ sig | PFix of Term.fixpoint | PCoFix of Term.cofixpoint - type constr_under_binders = Names.Id.t list * EConstr.constr - - (** Types of substitutions with or w/o bound variables *) - - type patvar_map = EConstr.constr Names.Id.Map.t - type extended_patvar_map = constr_under_binders Names.Id.Map.t - end module Namegen : @@ -2737,15 +2779,15 @@ sig the whole identifier except for the {i subscript}. E.g. if we take [foo42], then [42] is the {i subscript}, and [foo] is the root. *) - val next_ident_away : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> string val id_of_name_using_hdchar : Environ.env -> Evd.evar_map -> EConstr.types -> Names.Name.t -> Names.Id.t - val next_ident_away_in_goal : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_ident_away_in_goal : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val default_dependent_ident : Names.Id.t - val next_global_ident_away : Names.Id.t -> Names.Id.t list -> Names.Id.t + val next_global_ident_away : Names.Id.t -> Names.Id.Set.t -> Names.Id.t val rename_bound_vars_as_displayed : - Evd.evar_map -> Names.Id.t list -> Names.Name.t list -> EConstr.types -> EConstr.types + Evd.evar_map -> Names.Id.Set.t -> Names.Name.t list -> EConstr.types -> EConstr.types end module Termops : @@ -2753,9 +2795,10 @@ sig val it_mkLambda_or_LetIn : Constr.t -> Context.Rel.t -> Constr.t val local_occur_var : Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool val occur_var : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool - val pr_evar_info : Evd.evar_info -> Pp.std_ppcmds + val pr_evar_info : Evd.evar_info -> Pp.t - val print_constr : EConstr.constr -> Pp.std_ppcmds + val print_constr : EConstr.constr -> Pp.t + val pr_sort_family : Sorts.family -> Pp.t (** [dependent m t] tests whether [m] is a subterm of [t] *) val dependent : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool @@ -2799,10 +2842,12 @@ sig val ids_of_named_context : ('c, 't) Context.Named.pt -> Names.Id.t list val ids_of_context : Environ.env -> Names.Id.t list val global_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference * EConstr.EInstance.t - val print_named_context : Environ.env -> Pp.std_ppcmds - val print_constr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.std_ppcmds + val print_named_context : Environ.env -> Pp.t + val print_constr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val clear_named_body : Names.Id.t -> Environ.env -> Environ.env val is_Prop : Evd.evar_map -> EConstr.constr -> bool + val is_Set : Evd.evar_map -> EConstr.constr -> bool + val is_Type : Evd.evar_map -> EConstr.constr -> bool val is_global : Evd.evar_map -> Globnames.global_reference -> EConstr.constr -> bool val eq_constr : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool @@ -2821,14 +2866,14 @@ sig val replace_term : Evd.evar_map -> EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt - val pr_metaset : Evd.Metaset.t -> Pp.std_ppcmds - val pr_evar_map : ?with_univs:bool -> int option -> Evd.evar_map -> Pp.std_ppcmds - val pr_evar_universe_context : UState.t -> Pp.std_ppcmds + val pr_metaset : Evd.Metaset.t -> Pp.t + val pr_evar_map : ?with_univs:bool -> int option -> Evd.evar_map -> Pp.t + val pr_evar_universe_context : UState.t -> Pp.t end module Proofview_monad : sig - type lazy_msg = unit -> Pp.std_ppcmds + type lazy_msg = unit -> Pp.t module Info : sig type tree @@ -2904,10 +2949,10 @@ sig val ( >> ) : unit t -> 'a t -> 'a t val ( >>= ) : 'a t -> ('a -> 'b t) -> 'b t val print_char : char -> unit t - val print_debug : Pp.std_ppcmds -> unit t - val print_warning : Pp.std_ppcmds -> unit t - val print_notice : Pp.std_ppcmds -> unit t - val print_info : Pp.std_ppcmds -> unit t + val print_debug : Pp.t -> unit t + val print_warning : Pp.t -> unit t + val print_notice : Pp.t -> unit t + val print_info : Pp.t -> unit t val run : 'a t -> 'a type 'a ref val ref : 'a -> 'a ref t @@ -3037,7 +3082,7 @@ sig | Opt : 'a tag -> 'a option tag | Pair : 'a tag * 'b tag -> ('a * 'b) tag val create : string -> 'a typ - val pr : 'a typ -> Pp.std_ppcmds + val pr : 'a typ -> Pp.t val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option val typ_list : t list typ val typ_opt : t option typ @@ -3071,83 +3116,67 @@ end (* XXX: Located manually from intf *) module Glob_term : sig - type cases_pattern_r = + type 'a cases_pattern_r = | PatVar of Names.Name.t - | PatCstr of Names.constructor * cases_pattern list * Names.Name.t - and cases_pattern = cases_pattern_r CAst.t + | PatCstr of Names.constructor * 'a cases_pattern_g list * Names.Name.t + and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t + type cases_pattern = [ `any ] cases_pattern_g type existential_name = Names.Id.t - type glob_constr_r = + type 'a glob_constr_r = | GRef of Globnames.global_reference * Misctypes.glob_level list option (** An identifier that represents a reference to an object defined either in the (global) environment or in the (local) context. *) | GVar of Names.Id.t (** An identifier that cannot be regarded as "GRef". Bound variables are typically represented this way. *) - | GEvar of existential_name * (Names.Id.t * glob_constr) list + | GEvar of existential_name * (Names.Id.t * 'a glob_constr_g) list | GPatVar of Evar_kinds.matching_var_kind - | GApp of glob_constr * glob_constr list - | GLambda of Names.Name.t * Decl_kinds.binding_kind * glob_constr * glob_constr - | GProd of Names.Name.t * Decl_kinds.binding_kind * glob_constr * glob_constr - | GLetIn of Names.Name.t * glob_constr * glob_constr option * glob_constr - | GCases of Term.case_style * glob_constr option * tomatch_tuples * cases_clauses - | GLetTuple of Names.Name.t list * (Names.Name.t * glob_constr option) * glob_constr * glob_constr - | GIf of glob_constr * (Names.Name.t * glob_constr option) * glob_constr * glob_constr - | GRec of fix_kind * Names.Id.t array * glob_decl list array * - glob_constr array * glob_constr array + | GApp of 'a glob_constr_g * 'a glob_constr_g list + | GLambda of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g + | GProd of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g + | GLetIn of Names.Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g + | GCases of Term.case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g + | GLetTuple of Names.Name.t list * (Names.Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g + | GIf of 'a glob_constr_g * (Names.Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g + | GRec of 'a fix_kind_g * Names.Id.t array * 'a glob_decl_g list array * + 'a glob_constr_g array * 'a glob_constr_g array | GSort of Misctypes.glob_sort | GHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option - | GCast of glob_constr * glob_constr Misctypes.cast_type + | GCast of 'a glob_constr_g * 'a glob_constr_g Misctypes.cast_type - and glob_constr = glob_constr_r CAst.t + and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t - and glob_decl = Names.Name.t * Decl_kinds.binding_kind * glob_constr option * glob_constr + and 'a glob_decl_g = Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g option * 'a glob_constr_g - and fix_recursion_order = + and 'a fix_recursion_order_g = | GStructRec - | GWfRec of glob_constr - | GMeasureRec of glob_constr * glob_constr option + | GWfRec of 'a glob_constr_g + | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option - and fix_kind = - | GFix of ((int option * fix_recursion_order) array * int) + and 'a fix_kind_g = + | GFix of ((int option * 'a fix_recursion_order_g) array * int) | GCoFix of int - and predicate_pattern = + and 'a predicate_pattern_g = Names.Name.t * (Names.inductive * Names.Name.t list) Loc.located option - and tomatch_tuple = (glob_constr * predicate_pattern) - - and tomatch_tuples = tomatch_tuple list - - and cases_clause = (Names.Id.t list * cases_pattern list * glob_constr) Loc.located - and cases_clauses = cases_clause list - - (** A globalised term together with a closure representing the value - of its free variables. Intended for use when these variables are taken - from the Ltac environment. *) - - type closure = { - idents : Names.Id.t Names.Id.Map.t; - typed : Pattern.constr_under_binders Names.Id.Map.t ; - untyped: closed_glob_constr Names.Id.Map.t } - and closed_glob_constr = { - closure: closure; - term: glob_constr } - - (** Ltac variable maps *) - type var_map = Pattern.constr_under_binders Names.Id.Map.t - type uconstr_var_map = closed_glob_constr Names.Id.Map.t - type unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.t - - type ltac_var_map = { - ltac_constrs : var_map; - (** Ltac variables bound to constrs *) - ltac_uconstrs : uconstr_var_map; - (** Ltac variables bound to untyped constrs *) - ltac_idents: Names.Id.t Names.Id.Map.t; - (** Ltac variables bound to identifiers *) - ltac_genargs : unbound_ltac_var_map; - (** Ltac variables bound to other kinds of arguments *) - } + and 'a tomatch_tuple_g = ('a glob_constr_g * 'a predicate_pattern_g) + + and 'a tomatch_tuples_g = 'a tomatch_tuple_g list + + and 'a cases_clause_g = (Names.Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) Loc.located + and 'a cases_clauses_g = 'a cases_clause_g list + + type glob_constr = [ `any ] glob_constr_g + type tomatch_tuple = [ `any ] tomatch_tuple_g + type tomatch_tuples = [ `any ] tomatch_tuples_g + type cases_clause = [ `any ] cases_clause_g + type cases_clauses = [ `any ] cases_clauses_g + type glob_decl = [ `any ] glob_decl_g + type fix_kind = [ `any ] fix_kind_g + type predicate_pattern = [ `any ] predicate_pattern_g + type any_glob_constr = + | AnyGlobConstr : 'r glob_constr_g -> any_glob_constr end @@ -3183,6 +3212,10 @@ sig | NCast of notation_constr * notation_constr Misctypes.cast_type type interpretation = (Names.Id.t * (subscopes * notation_var_instance_type)) list * notation_constr + type precedence = int + type parenRelation = + | L | E | Any | Prec of precedence + type tolerability = precedence * parenRelation end module Tactypes : @@ -3208,6 +3241,79 @@ end (* Modules from pretyping/ *) (************************************************************************) +module Ltac_pretype : +sig +open Names +open Glob_term + +(** {5 Maps of pattern variables} *) + +(** Type [constr_under_binders] is for representing the term resulting + of a matching. Matching can return terms defined in a some context + of named binders; in the context, variable names are ordered by + (<) and referred to by index in the term Thanks to the canonical + ordering, a matching problem like + + [match ... with [(fun x y => ?p,fun y x => ?p)] => [forall x y => p]] + + will be accepted. Thanks to the reference by index, a matching + problem like + + [match ... with [(fun x => ?p)] => [forall x => p]] + + will work even if [x] is also the name of an existing goal + variable. + + Note: we do not keep types in the signature. Besides simplicity, + the main reason is that it would force to close the signature over + binders that occur only in the types of effective binders but not + in the term itself (e.g. for a term [f x] with [f:A -> True] and + [x:A]). + + On the opposite side, by not keeping the types, we loose + opportunity to propagate type informations which otherwise would + not be inferable, as e.g. when matching [forall x, x = 0] with + pattern [forall x, ?h = 0] and using the solution "x|-h:=x" in + expression [forall x, h = x] where nothing tells how the type of x + could be inferred. We also loose the ability of typing ltac + variables before calling the right-hand-side of ltac matching clauses. *) + +type constr_under_binders = Id.t list * EConstr.constr + +(** Types of substitutions with or w/o bound variables *) + +type patvar_map = EConstr.constr Id.Map.t +type extended_patvar_map = constr_under_binders Id.Map.t + +(** A globalised term together with a closure representing the value + of its free variables. Intended for use when these variables are taken + from the Ltac environment. *) +type closure = { + idents:Id.t Id.Map.t; + typed: constr_under_binders Id.Map.t ; + untyped:closed_glob_constr Id.Map.t } +and closed_glob_constr = { + closure: closure; + term: glob_constr } + +(** Ltac variable maps *) +type var_map = constr_under_binders Id.Map.t +type uconstr_var_map = closed_glob_constr Id.Map.t +type unbound_ltac_var_map = Geninterp.Val.t Id.Map.t + +type ltac_var_map = { + ltac_constrs : var_map; + (** Ltac variables bound to constrs *) + ltac_uconstrs : uconstr_var_map; + (** Ltac variables bound to untyped constrs *) + ltac_idents: Id.t Id.Map.t; + (** Ltac variables bound to identifiers *) + ltac_genargs : unbound_ltac_var_map; + (** Ltac variables bound to other kinds of arguments *) +} + +end + module Locusops : sig val clause_with_generic_occurrences : 'a Locus.clause_expr -> bool @@ -3290,16 +3396,16 @@ sig val nf_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr val nf_meta : Evd.evar_map -> EConstr.constr -> EConstr.constr val hnf_prod_appvect : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr array -> EConstr.constr - val pr_state : state -> Pp.std_ppcmds + val pr_state : state -> Pp.t module Stack : sig type 'a t - val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + val pr : ('a -> Pp.t) -> 'a t -> Pp.t end module Cst_stack : sig type t - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t end end @@ -3445,7 +3551,7 @@ sig val map_glob_constr : (Glob_term.glob_constr -> Glob_term.glob_constr) -> Glob_term.glob_constr -> Glob_term.glob_constr - val empty_lvar : Glob_term.ltac_var_map + val empty_lvar : Ltac_pretype.ltac_var_map end @@ -3461,7 +3567,7 @@ sig val subst_pattern : Mod_subst.substitution -> Pattern.constr_pattern -> Pattern.constr_pattern val pattern_of_constr : Environ.env -> Evd.evar_map -> Constr.t -> Pattern.constr_pattern val instantiate_pattern : Environ.env -> - Evd.evar_map -> Pattern.extended_patvar_map -> + Evd.evar_map -> Ltac_pretype.extended_patvar_map -> Pattern.constr_pattern -> Pattern.constr_pattern end @@ -3474,16 +3580,16 @@ sig val is_matching : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> bool val extended_matches : Environ.env -> Evd.evar_map -> binding_bound_vars * Pattern.constr_pattern -> - EConstr.constr -> bound_ident_map * Pattern.extended_patvar_map + EConstr.constr -> bound_ident_map * Ltac_pretype.extended_patvar_map exception PatternMatchingFailure type matching_result = - { m_sub : bound_ident_map * Pattern.patvar_map; + { 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 matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Pattern.patvar_map + val matches : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> EConstr.constr -> Ltac_pretype.patvar_map end module Tacred : @@ -3637,7 +3743,7 @@ sig type lname = Names.Name.t Loc.located type lident = Names.Id.t Loc.located type opacity_flag = - | Opaque of lident list option + | Opaque | Transparent type locality_flag = bool type inductive_kind = @@ -3650,7 +3756,7 @@ sig | VtProofStep of proof_step | VtProofMode of string | VtQuery of vernac_part_of_script * Feedback.route_id - | VtStm of vernac_control * vernac_part_of_script + | VtMeta | VtUnknown and vernac_qed_type = | VtKeep @@ -3659,10 +3765,6 @@ sig and vernac_start = string * opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and vernac_part_of_script = bool - and vernac_control = - | VtWait - | VtJoinDocument - | VtBack of Stateid.t and opacity_guarantee = | GuaranteesOpacity | Doesn'tGuaranteeOpacity @@ -3682,6 +3784,10 @@ sig 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 + type lstring type 'a with_coercion = coercion_flag * 'a type scope_name = string @@ -3699,9 +3805,7 @@ sig | Constructors of constructor_expr list | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list - type plident = lident * lident list option - - type inductive_expr = plident with_coercion * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * inductive_kind * constructor_list_or_record_decl_expr + type inductive_expr = ident_decl with_coercion * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * inductive_kind * constructor_list_or_record_decl_expr type syntax_modifier = | SetItemLevel of string list * Extend.production_level @@ -3715,18 +3819,20 @@ sig type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation + type typeclass_constraint = (Names.Name.t Loc.located * universe_decl_expr option) * Decl_kinds.binding_kind * constr_expr + type definition_expr = | ProveBody of local_binder_expr list * constr_expr | DefineBody of local_binder_expr list * Genredexpr.raw_red_expr option * constr_expr * constr_expr option type proof_expr = - plident option * (local_binder_expr list * constr_expr) + ident_decl option * (local_binder_expr list * constr_expr) type proof_end = | Admitted | Proved of opacity_flag * lident option - type fixpoint_expr = plident * (Names.Id.t Loc.located option * Constrexpr.recursion_order_expr) * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr option + type fixpoint_expr = ident_decl * (Names.Id.t Loc.located option * Constrexpr.recursion_order_expr) * Constrexpr.local_binder_expr list * Constrexpr.constr_expr * Constrexpr.constr_expr option type cofixpoint_expr @@ -3744,7 +3850,6 @@ sig type option_value type showable type bullet - type stm_vernac type comment type register_kind type locatable @@ -3781,6 +3886,12 @@ sig | DefaultInline | InlineAt of int + type cumulative_inductive_parsing_flag = + | GlobalCumulativity + | GlobalNonCumulativity + | LocalCumulativity + | LocalNonCumulativity + type vernac_expr = | VernacLoad of verbose_flag * string | VernacTime of vernac_expr Loc.located @@ -3788,7 +3899,7 @@ sig | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr | VernacSyntaxExtension of - obsolete_locality * (lstring * syntax_modifier list) + bool * obsolete_locality * (lstring * syntax_modifier list) | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * class_rawexpr list @@ -3799,13 +3910,13 @@ sig scope_name option | VernacNotationAddFormat of string * string * string | VernacDefinition of - (Decl_kinds.locality option * Decl_kinds.definition_object_kind) * plident * definition_expr + (Decl_kinds.locality option * 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) * - inline * (plident list * Constrexpr.constr_expr) with_coercion list - | VernacInductive of Decl_kinds.cumulative_inductive_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + 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 | VernacCoFixpoint of @@ -3828,7 +3939,7 @@ sig | VernacInstance of bool * Constrexpr.local_binder_expr list * - Constrexpr.typeclass_constraint * + typeclass_constraint * (bool * Constrexpr.constr_expr) option * hint_info_expr | VernacContext of Constrexpr.local_binder_expr list @@ -3890,7 +4001,6 @@ sig | VernacLocate of locatable | VernacRegister of lident * register_kind | VernacComments of comment list - | VernacStm of stm_vernac | VernacGoal of Constrexpr.constr_expr | VernacAbort of lident option | VernacAbortAll @@ -3920,7 +4030,7 @@ sig | SelectAll and vernac_classification = vernac_type * vernac_when and one_inductive_expr = - plident * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list + ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list end (* XXX: end manual intf move *) @@ -3964,16 +4074,19 @@ sig EConstr.types * inheritance_path val get_coercion_value : coe_index -> Constr.t val coercions : unit -> coe_index list - val pr_cl_index : cl_index -> Pp.std_ppcmds + val pr_cl_index : cl_index -> Pp.t end module Detyping : sig + type 'a delay = + | Now : 'a delay + | Later : [ `thunk ] delay val print_universes : bool ref val print_evar_arguments : bool ref - val detype : ?lax:bool -> bool -> Names.Id.t list -> Environ.env -> Evd.evar_map -> EConstr.constr -> Glob_term.glob_constr + 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 -> Glob_term.glob_constr) -> unit + val set_detype_anonymous : (?loc:Loc.t -> int -> Names.Id.t) -> unit end module Indrec : @@ -4006,29 +4119,21 @@ sig expand_evars : bool } - type pure_open_constr = Evd.evar_map * EConstr.constr - type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr - val understand_ltac : inference_flags -> - Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map -> - typing_constraint -> Glob_term.glob_constr -> pure_open_constr + Environ.env -> Evd.evar_map -> Ltac_pretype.ltac_var_map -> + typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.t val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map -> ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr - val type_uconstr : - ?flags:inference_flags -> - ?expected_type:typing_constraint -> - Geninterp.interp_sign -> Glob_term.closed_glob_constr -> EConstr.constr Tactypes.delayed_open val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Constr.t Evd.in_evar_universe_context val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit - val interp_elimination_sort : Misctypes.glob_sort -> Sorts.family val register_constr_interp0 : ('r, 'g, 't) Genarg.genarg_type -> - (Glob_term.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit + (Ltac_pretype.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit val all_and_fail_flags : inference_flags val ise_pretype_gen : inference_flags -> Environ.env -> Evd.evar_map -> - Glob_term.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr + Ltac_pretype.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr end module Unification : @@ -4062,6 +4167,18 @@ sig Environ.env -> Evd.evar_map -> ?flags:unify_flags -> EConstr.constr * EConstr.constr -> Evd.evar_map * EConstr.constr end +module Univdecls : +sig + type universe_decl = + (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl + + val interp_univ_decl : Environ.env -> Vernacexpr.universe_decl_expr -> + Evd.evar_map * universe_decl + val interp_univ_decl_opt : Environ.env -> Vernacexpr.universe_decl_expr option -> + Evd.evar_map * universe_decl + val default_univ_decl : universe_decl +end + (************************************************************************) (* End of modules from pretyping/ *) (************************************************************************) @@ -4117,13 +4234,14 @@ sig val wit_global : (Libnames.reference, Globnames.global_reference Loc.located Misctypes.or_var, Globnames.global_reference) Genarg.genarg_type val wit_ident : Names.Id.t Genarg.uniform_genarg_type val wit_integer : int Genarg.uniform_genarg_type + val wit_sort_family : (Sorts.family, unit, unit) Genarg.genarg_type val wit_constr : (Constrexpr.constr_expr, Tactypes.glob_constr_and_expr, EConstr.constr) Genarg.genarg_type val wit_open_constr : (Constrexpr.constr_expr, Tactypes.glob_constr_and_expr, EConstr.constr) Genarg.genarg_type val wit_intro_pattern : (Constrexpr.constr_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.glob_constr_and_expr Misctypes.intro_pattern_expr Loc.located, Tactypes.intro_pattern) Genarg.genarg_type val wit_int_or_var : (int Misctypes.or_var, int Misctypes.or_var, int) Genarg.genarg_type val wit_ref : (Libnames.reference, Globnames.global_reference Loc.located Misctypes.or_var, Globnames.global_reference) Genarg.genarg_type val wit_clause_dft_concl : (Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Loc.located Locus.clause_expr,Names.Id.t Locus.clause_expr) Genarg.genarg_type - val wit_uconstr : (Constrexpr.constr_expr , Tactypes.glob_constr_and_expr, Glob_term.closed_glob_constr) Genarg.genarg_type + val wit_uconstr : (Constrexpr.constr_expr , Tactypes.glob_constr_and_expr, Ltac_pretype.closed_glob_constr) Genarg.genarg_type val wit_red_expr : ((Constrexpr.constr_expr,Libnames.reference Misctypes.or_by_notation,Constrexpr.constr_expr) Genredexpr.red_expr_gen, (Tactypes.glob_constr_and_expr,Names.evaluable_global_reference Misctypes.and_short_name Misctypes.or_var,Tactypes.glob_constr_pattern_and_expr) Genredexpr.red_expr_gen, @@ -4172,22 +4290,12 @@ sig 'a -> Notation_term.notation_constr -> Glob_term.glob_constr end -module Ppextend : -sig - - type precedence = int - type parenRelation = - | L | E | Any | Prec of precedence - type tolerability = precedence * parenRelation - -end - module Notation : sig type cases_pattern_status = bool type required_module = Libnames.full_path * string list type 'a prim_token_interpreter = ?loc:Loc.t -> 'a -> Glob_term.glob_constr - type 'a prim_token_uninterpreter = Glob_term.glob_constr list * (Glob_term.glob_constr -> 'a option) * cases_pattern_status + type 'a prim_token_uninterpreter = Glob_term.glob_constr list * (Glob_term.any_glob_constr -> 'a option) * cases_pattern_status type delimiters = string type local_scopes = Notation_term.tmp_scope_name option * Notation_term.scope_name list type notation_location = (Names.DirPath.t * Names.DirPath.t) * string @@ -4197,11 +4305,11 @@ sig Bigint.bigint prim_token_interpreter -> Bigint.bigint prim_token_uninterpreter -> unit val interp_notation_as_global_reference : ?loc:Loc.t -> (Globnames.global_reference -> bool) -> Constrexpr.notation -> delimiters option -> Globnames.global_reference - val locate_notation : (Glob_term.glob_constr -> Pp.std_ppcmds) -> Constrexpr.notation -> - Notation_term.scope_name option -> Pp.std_ppcmds + val locate_notation : (Glob_term.glob_constr -> Pp.t) -> Constrexpr.notation -> + Notation_term.scope_name option -> Pp.t val find_delimiters_scope : ?loc:Loc.t -> delimiters -> Notation_term.scope_name - val pr_scope : (Glob_term.glob_constr -> Pp.std_ppcmds) -> Notation_term.scope_name -> Pp.std_ppcmds - val pr_scopes : (Glob_term.glob_constr -> Pp.std_ppcmds) -> Pp.std_ppcmds + val pr_scope : (Glob_term.glob_constr -> Pp.t) -> Notation_term.scope_name -> Pp.t + val pr_scopes : (Glob_term.glob_constr -> Pp.t) -> Pp.t val interp_notation : ?loc:Loc.t -> Constrexpr.notation -> local_scopes -> Notation_term.interpretation * (notation_location * Notation_term.scope_name option) val uninterp_prim_token : Glob_term.glob_constr -> Notation_term.scope_name * Constrexpr.prim_token @@ -4282,10 +4390,10 @@ module Constrextern : sig val extern_glob_constr : Names.Id.Set.t -> Glob_term.glob_constr -> Constrexpr.constr_expr val extern_glob_type : Names.Id.Set.t -> Glob_term.glob_constr -> Constrexpr.constr_expr - val extern_constr : ?lax:bool -> bool -> Environ.env -> Evd.evar_map -> Constr.t -> Constrexpr.constr_expr + val extern_constr : ?lax:bool -> bool -> Environ.env -> Evd.evar_map -> EConstr.t -> Constrexpr.constr_expr val without_symbols : ('a -> 'b) -> 'a -> 'b val print_universes : bool ref - val extern_type : bool -> Environ.env -> Evd.evar_map -> Term.types -> Constrexpr.constr_expr + val extern_type : bool -> Environ.env -> Evd.evar_map -> EConstr.t -> Constrexpr.constr_expr val with_universes : ('a -> 'b) -> 'a -> 'b val set_extern_reference : (?loc:Loc.t -> Names.Id.Set.t -> Globnames.global_reference -> Libnames.reference) -> unit @@ -4334,19 +4442,19 @@ end module Miscprint : sig val pr_or_and_intro_pattern : - ('a -> Pp.std_ppcmds) -> 'a Misctypes.or_and_intro_pattern_expr -> Pp.std_ppcmds - val pr_intro_pattern_naming : Misctypes.intro_pattern_naming_expr -> Pp.std_ppcmds + ('a -> Pp.t) -> 'a Misctypes.or_and_intro_pattern_expr -> Pp.t + val pr_intro_pattern_naming : Misctypes.intro_pattern_naming_expr -> Pp.t val pr_intro_pattern : - ('a -> Pp.std_ppcmds) -> 'a Misctypes.intro_pattern_expr Loc.located -> Pp.std_ppcmds + ('a -> Pp.t) -> 'a Misctypes.intro_pattern_expr Loc.located -> Pp.t val pr_bindings : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a Misctypes.bindings -> Pp.std_ppcmds + ('a -> Pp.t) -> + ('a -> Pp.t) -> 'a Misctypes.bindings -> Pp.t val pr_bindings_no_with : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a Misctypes.bindings -> Pp.std_ppcmds + ('a -> Pp.t) -> + ('a -> Pp.t) -> 'a Misctypes.bindings -> Pp.t val pr_with_bindings : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a * 'a Misctypes.bindings -> Pp.std_ppcmds + ('a -> Pp.t) -> + ('a -> Pp.t) -> 'a * 'a Misctypes.bindings -> Pp.t end (* All items in the Goal modules are deprecated. *) @@ -4354,7 +4462,7 @@ module Goal : sig type goal = Evar.t - val pr_goal : goal -> Pp.std_ppcmds + val pr_goal : goal -> Pp.t module V82 : sig @@ -4386,16 +4494,16 @@ end module Evar_refiner : sig + type glob_constr_ltac_closure = Ltac_pretype.ltac_var_map * Glob_term.glob_constr + val w_refine : Evar.t * Evd.evar_info -> - Pretyping.glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map + glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map end module Proof_type : sig - type prim_rule = - | Cut of bool * bool * Names.Id.t * Term.types - | Refine of Constr.t + type prim_rule = Refine of Constr.t type tactic = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma end @@ -4431,7 +4539,7 @@ sig 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.std_ppcmds + val pr_proof : proof -> Pp.t module V82 : sig val grab_evars : proof -> proof @@ -4447,6 +4555,9 @@ end module Proof_global : sig + + type state + type proof_mode = { name : string; set : unit -> unit ; @@ -4469,12 +4580,11 @@ sig type proof_terminator type lemma_possible_guards - type universe_binders type closed_proof = proof_object * proof_terminator val make_terminator : (proof_ending -> unit) -> proof_terminator val start_dependent_proof : - Names.Id.t -> ?pl:universe_binders -> Decl_kinds.goal_kind -> + 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 @@ -4510,13 +4620,13 @@ sig val repackage : Evd.evar_map ref -> 'a -> 'a Evd.sigma val tclSHOWHYPS : Proof_type.tactic -> Proof_type.tactic - exception FailError of int * Pp.std_ppcmds Lazy.t + exception FailError of int * Pp.t Lazy.t val tclEVARS : Evd.evar_map -> Proof_type.tactic val tclMAP : ('a -> Proof_type.tactic) -> 'a list -> Proof_type.tactic val tclREPEAT : Proof_type.tactic -> Proof_type.tactic val tclORELSE : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic - val tclFAIL : int -> Pp.std_ppcmds -> Proof_type.tactic + val tclFAIL : int -> Pp.t -> Proof_type.tactic val tclIDTAC : Proof_type.tactic val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic val tclTHENLIST : Proof_type.tactic list -> Proof_type.tactic @@ -4575,7 +4685,7 @@ sig val pf_hyps_types : Goal.goal Evd.sigma -> (Names.Id.t * EConstr.types) list - val pr_gls : Goal.goal Evd.sigma -> Pp.std_ppcmds + val pr_gls : Goal.goal Evd.sigma -> Pp.t val pf_nf_betaiota : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr @@ -4594,8 +4704,10 @@ sig val pf_env : 'a Proofview.Goal.t -> Environ.env val pf_ids_of_hyps : 'a Proofview.Goal.t -> Names.Id.t list + val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Names.Id.Set.t val pf_concl : 'a Proofview.Goal.t -> EConstr.types val pf_get_new_id : Names.Id.t -> 'a Proofview.Goal.t -> Names.Id.t + val pf_get_hyp : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.named_declaration val pf_get_hyp_typ : Names.Id.t -> 'a Proofview.Goal.t -> EConstr.types val pf_get_type_of : 'a Proofview.Goal.t -> EConstr.constr -> EConstr.types val pf_global : Names.Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference @@ -4626,6 +4738,7 @@ sig val get_current_proof_name : unit -> Names.Id.t [@@ocaml.deprecated "use Proof_global.get_current_proof_name"] + val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types end module Clenv : @@ -4648,7 +4761,7 @@ sig val solve_evar_clause : Environ.env -> Evd.evar_map -> bool -> clause -> EConstr.constr Misctypes.bindings -> Evd.evar_map type clausenv - val pr_clenv : clausenv -> Pp.std_ppcmds + val pr_clenv : clausenv -> Pp.t end (************************************************************************) @@ -4687,7 +4800,7 @@ sig type coq_parsable - val parsable : ?file:string -> char Stream.t -> coq_parsable + val parsable : ?file:Loc.source -> char Stream.t -> coq_parsable val action : 'a -> action val entry_create : string -> 'a entry val entry_parse : 'a entry -> coq_parsable -> 'a @@ -4757,6 +4870,7 @@ sig val global : reference Gram.entry val universe_level : glob_level Gram.entry val sort : glob_sort Gram.entry + val sort_family : Sorts.family Gram.entry val pattern : cases_pattern_expr Gram.entry val constr_pattern : constr_expr Gram.entry val lconstr_pattern : constr_expr Gram.entry @@ -4833,6 +4947,22 @@ sig end +module G_vernac : +sig + + val def_body : Vernacexpr.definition_expr Pcoq.Gram.entry + val section_subset_expr : Vernacexpr.section_subset_expr Pcoq.Gram.entry + val query_command : (Vernacexpr.goal_selector option -> Vernacexpr.vernac_expr) Pcoq.Gram.entry + +end + +module G_proofs : +sig + + val hint : Vernacexpr.hints_expr Pcoq.Gram.entry + +end + (************************************************************************) (* End of modules from parsing/ *) (************************************************************************) @@ -4843,7 +4973,7 @@ end module Genprint : sig - type 'a printer = 'a -> Pp.std_ppcmds + type 'a printer = 'a -> Pp.t val generic_top_print : Genarg.tlevel Genarg.generic_argument printer val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw printer -> 'glb printer -> 'top printer -> unit @@ -4851,74 +4981,89 @@ end module Pputils : sig - val pr_with_occurrences : ('a -> Pp.std_ppcmds) -> (string -> Pp.std_ppcmds) -> 'a Locus.with_occurrences -> Pp.std_ppcmds + val pr_with_occurrences : ('a -> Pp.t) -> (string -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t val pr_red_expr : - ('a -> Pp.std_ppcmds) * ('a -> Pp.std_ppcmds) * ('b -> Pp.std_ppcmds) * ('c -> Pp.std_ppcmds) -> - (string -> Pp.std_ppcmds) -> - ('a,'b,'c) Genredexpr.red_expr_gen -> Pp.std_ppcmds - val pr_raw_generic : Environ.env -> Genarg.rlevel Genarg.generic_argument -> Pp.std_ppcmds - val pr_glb_generic : Environ.env -> Genarg.glevel Genarg.generic_argument -> Pp.std_ppcmds - val pr_or_var : ('a -> Pp.std_ppcmds) -> 'a Misctypes.or_var -> Pp.std_ppcmds - val pr_or_by_notation : ('a -> Pp.std_ppcmds) -> 'a Misctypes.or_by_notation -> Pp.std_ppcmds + ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> + (string -> Pp.t) -> + ('a,'b,'c) Genredexpr.red_expr_gen -> Pp.t + val pr_raw_generic : Environ.env -> Genarg.rlevel Genarg.generic_argument -> Pp.t + val pr_glb_generic : Environ.env -> Genarg.glevel Genarg.generic_argument -> Pp.t + val pr_or_var : ('a -> Pp.t) -> 'a Misctypes.or_var -> Pp.t + val pr_or_by_notation : ('a -> Pp.t) -> 'a Misctypes.or_by_notation -> Pp.t end module Ppconstr : sig - val pr_name : Names.Name.t -> Pp.std_ppcmds + val pr_name : Names.Name.t -> Pp.t [@@ocaml.deprecated "alias of API.Names.Name.print"] - val pr_id : Names.Id.t -> Pp.std_ppcmds - val pr_or_var : ('a -> Pp.std_ppcmds) -> 'a Misctypes.or_var -> Pp.std_ppcmds - val pr_with_comments : ?loc:Loc.t -> Pp.std_ppcmds -> Pp.std_ppcmds - val pr_lident : Names.Id.t Loc.located -> Pp.std_ppcmds - val pr_lname : Names.Name.t Loc.located -> Pp.std_ppcmds - val prec_less : int -> int * Ppextend.parenRelation -> bool - val pr_constr_expr : Constrexpr.constr_expr -> Pp.std_ppcmds - val pr_lconstr_expr : Constrexpr.constr_expr -> Pp.std_ppcmds - val pr_constr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.std_ppcmds - val pr_lconstr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.std_ppcmds - val pr_binders : Constrexpr.local_binder_expr list -> Pp.std_ppcmds - val pr_glob_sort : Misctypes.glob_sort -> Pp.std_ppcmds + val pr_id : Names.Id.t -> Pp.t + val pr_or_var : ('a -> Pp.t) -> 'a Misctypes.or_var -> Pp.t + val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t + val pr_lident : Names.Id.t Loc.located -> Pp.t + val pr_lname : Names.Name.t Loc.located -> Pp.t + val prec_less : int -> int * Notation_term.parenRelation -> bool + val pr_constr_expr : Constrexpr.constr_expr -> Pp.t + val pr_lconstr_expr : Constrexpr.constr_expr -> Pp.t + val pr_constr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.t + val pr_lconstr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.t + val pr_binders : Constrexpr.local_binder_expr list -> Pp.t + val pr_glob_sort : Misctypes.glob_sort -> Pp.t end module Printer : sig - val pr_named_context : Environ.env -> Evd.evar_map -> Context.Named.t -> Pp.std_ppcmds - val pr_rel_context : Environ.env -> Evd.evar_map -> Context.Rel.t -> Pp.std_ppcmds - val pr_goal : Goal.goal Evd.sigma -> Pp.std_ppcmds - - val pr_constr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.std_ppcmds - val pr_lconstr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.std_ppcmds - - val pr_constr : Constr.t -> Pp.std_ppcmds - - val pr_lconstr : Constr.t -> Pp.std_ppcmds - - val pr_econstr : EConstr.constr -> Pp.std_ppcmds - val pr_glob_constr : Glob_term.glob_constr -> Pp.std_ppcmds - val pr_constr_pattern : Pattern.constr_pattern -> Pp.std_ppcmds - val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.std_ppcmds - val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.std_ppcmds - val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.std_ppcmds - val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.std_ppcmds - val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.std_ppcmds - val pr_closed_glob : Glob_term.closed_glob_constr -> Pp.std_ppcmds - val pr_lglob_constr : Glob_term.glob_constr -> Pp.std_ppcmds - val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.std_ppcmds - val pr_leconstr : EConstr.constr -> Pp.std_ppcmds - val pr_global : Globnames.global_reference -> Pp.std_ppcmds - val pr_lconstr_under_binders : Pattern.constr_under_binders -> Pp.std_ppcmds - val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.std_ppcmds - - val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.std_ppcmds - val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Glob_term.closed_glob_constr -> Pp.std_ppcmds - val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.std_ppcmds - val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.std_ppcmds - val pr_ltype : Term.types -> Pp.std_ppcmds - val pr_ljudge : EConstr.unsafe_judgment -> Pp.std_ppcmds * Pp.std_ppcmds - val pr_idpred : Names.Id.Pred.t -> Pp.std_ppcmds - val pr_cpred : Names.Cpred.t -> Pp.std_ppcmds - val pr_transparent_state : Names.transparent_state -> Pp.std_ppcmds + val pr_named_context : Environ.env -> Evd.evar_map -> Context.Named.t -> Pp.t + val pr_rel_context : Environ.env -> Evd.evar_map -> Context.Rel.t -> Pp.t + val pr_goal : Goal.goal Evd.sigma -> Pp.t + + val pr_constr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.t + val pr_lconstr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.t + + val pr_constr : Constr.t -> Pp.t + + val pr_lconstr : Constr.t -> Pp.t + + val pr_econstr : EConstr.constr -> Pp.t + val pr_glob_constr : Glob_term.glob_constr -> Pp.t + val pr_constr_pattern : Pattern.constr_pattern -> Pp.t + val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t + val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t + val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t + val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t + val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t + val pr_closed_glob : Ltac_pretype.closed_glob_constr -> Pp.t + val pr_lglob_constr : Glob_term.glob_constr -> Pp.t + val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t + val pr_leconstr : EConstr.constr -> Pp.t + val pr_global : Globnames.global_reference -> Pp.t + val pr_lconstr_under_binders : Ltac_pretype.constr_under_binders -> Pp.t + val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t + + val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Ltac_pretype.constr_under_binders -> Pp.t + val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Ltac_pretype.closed_glob_constr -> Pp.t + val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t + val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t + val pr_ltype : Term.types -> Pp.t + val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t + val pr_idpred : Names.Id.Pred.t -> Pp.t + val pr_cpred : Names.Cpred.t -> Pp.t + val pr_transparent_state : Names.transparent_state -> Pp.t +end + +module Prettyp : +sig + type 'a locatable_info = { + locate : Libnames.qualid -> 'a option; + locate_all : Libnames.qualid -> 'a list; + shortest_qualid : 'a -> Libnames.qualid; + name : 'a -> Pp.t; + print : 'a -> Pp.t; + about : 'a -> Pp.t; + } + + val register_locatable : string -> 'a locatable_info -> unit + val print_located_other : string -> Libnames.reference -> Pp.t end (************************************************************************) @@ -4936,7 +5081,7 @@ sig val tclORELSE : tactic -> tactic -> tactic val tclDO : int -> tactic -> tactic val tclIDTAC : tactic - val tclFAIL : int -> Pp.std_ppcmds -> tactic + val tclFAIL : int -> Pp.t -> tactic val tclTHEN : tactic -> tactic -> tactic val tclTHENLIST : tactic list -> tactic val pf_constr_of_global : @@ -4973,12 +5118,12 @@ sig sig open Proofview val tclORELSE0 : unit tactic -> unit tactic -> unit tactic - val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic + val tclFAIL : int -> Pp.t -> 'a tactic val pf_constr_of_global : Globnames.global_reference -> EConstr.constr tactic val tclTHEN : unit tactic -> unit tactic -> unit tactic val tclTHENS : unit tactic -> unit tactic list -> unit tactic val tclFIRST : unit tactic list -> unit tactic - val tclZEROMSG : ?loc:Loc.t -> Pp.std_ppcmds -> 'a tactic + val tclZEROMSG : ?loc:Loc.t -> Pp.t -> 'a tactic val tclORELSE : unit tactic -> unit tactic -> unit tactic val tclREPEAT : unit tactic -> unit tactic val tclTRY : unit tactic -> unit tactic @@ -5035,7 +5180,7 @@ sig val check_scheme : 'a scheme_kind -> Names.inductive -> bool val find_scheme : ?mode:Declare.internal_flag -> 'a scheme_kind -> Names.inductive -> Names.Constant.t * Safe_typing.private_constants - val pr_scheme_kind : 'a scheme_kind -> Pp.std_ppcmds + val pr_scheme_kind : 'a scheme_kind -> Pp.t end module Elimschemes : @@ -5051,7 +5196,7 @@ module Tactics : sig open Proofview - type change_arg = Pattern.patvar_map -> Evd.evar_map -> Evd.evar_map * EConstr.constr + type change_arg = Ltac_pretype.patvar_map -> Evd.evar_map -> Evd.evar_map * EConstr.constr type tactic_reduction = Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr type elim_scheme = @@ -5087,7 +5232,7 @@ sig val convert_concl : ?check:bool -> EConstr.types -> Constr.cast_kind -> unit tactic val intro_using : Names.Id.t -> unit tactic val intro : unit tactic - val fresh_id_in_env : Names.Id.t list -> Names.Id.t -> Environ.env -> Names.Id.t + val fresh_id_in_env : Names.Id.Set.t -> Names.Id.t -> Environ.env -> Names.Id.t val is_quantified_hypothesis : Names.Id.t -> 'a Goal.t -> bool val tclABSTRACT : ?opaque:bool -> Names.Id.t option -> unit Proofview.tactic -> unit Proofview.tactic val intro_patterns : bool -> Tactypes.intro_patterns -> unit Proofview.tactic @@ -5187,7 +5332,7 @@ sig val eapply_with_bindings : EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic val assert_by : Names.Name.t -> EConstr.types -> unit Proofview.tactic -> unit Proofview.tactic - val intro_avoiding : Names.Id.t list -> unit Proofview.tactic + val intro_avoiding : Names.Id.Set.t -> unit Proofview.tactic val pose_proof : Names.Name.t -> EConstr.constr -> unit Proofview.tactic val pattern_option : (Locus.occurrences * EConstr.constr) list -> Locus.goal_location -> unit Proofview.tactic val compute_elim_sig : Evd.evar_map -> ?elimc:EConstr.constr Misctypes.with_bindings -> EConstr.types -> elim_scheme @@ -5230,28 +5375,33 @@ sig | Naive | FirstSolved | AllMatches + type inj_flags = { + keep_proof_equalities : bool; (* One may want it or not *) + injection_in_context : bool; (* For regularity; one may want it from ML code but not interactively *) + injection_pattern_l2r_order : bool; (* Compatibility option: no reason not to want it *) + } val build_selector : Environ.env -> Evd.evar_map -> int -> EConstr.constr -> EConstr.types -> - EConstr.constr -> EConstr.constr -> Evd.evar_map * EConstr.constr + EConstr.constr -> EConstr.constr -> EConstr.constr val replace : EConstr.constr -> EConstr.constr -> unit Proofview.tactic val general_rewrite : orientation -> Locus.occurrences -> freeze_evars_flag -> dep_proof_flag -> ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr -> unit Proofview.tactic - val inj : Tactypes.intro_patterns option -> Misctypes.evars_flag -> + val inj : inj_flags option -> Tactypes.intro_patterns option -> Misctypes.evars_flag -> Misctypes.clear_flag -> EConstr.constr Misctypes.with_bindings -> unit Proofview.tactic val general_multi_rewrite : Misctypes.evars_flag -> (bool * Misctypes.multi * Misctypes.clear_flag * Tactypes.delayed_open_constr_with_bindings) list -> Locus.clause -> (unit Proofview.tactic * conditions) option -> unit Proofview.tactic val replace_in_clause_maybe_by : EConstr.constr -> EConstr.constr -> Locus.clause -> unit Proofview.tactic option -> unit Proofview.tactic val replace_term : bool option -> EConstr.constr -> Locus.clause -> unit Proofview.tactic - val dEq : Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic + val dEq : keep_proofs:bool option -> Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic val discr_tac : Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic - val injClause : Tactypes.intro_patterns option -> Misctypes.evars_flag -> + val injClause : inj_flags option -> Tactypes.intro_patterns option -> Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic - val simpleInjClause : Misctypes.evars_flag -> + val simpleInjClause : inj_flags option -> Misctypes.evars_flag -> EConstr.constr Misctypes.with_bindings Misctypes.destruction_arg option -> unit Proofview.tactic val rewriteInConcl : bool -> EConstr.constr -> unit Proofview.tactic @@ -5285,8 +5435,8 @@ sig ?tac:(unit Proofview.tactic * conditions) -> EConstr.constr Misctypes.with_bindings -> Misctypes.evars_flag -> unit Proofview.tactic val discriminable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool val discrHyp : Names.Id.t -> unit Proofview.tactic - val injectable : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool - val injHyp : Misctypes.clear_flag -> Names.Id.t -> unit Proofview.tactic + val injectable : Environ.env -> Evd.evar_map -> keep_proofs:(bool option) -> EConstr.constr -> EConstr.constr -> bool + val injHyp : inj_flags option -> Misctypes.clear_flag -> Names.Id.t -> unit Proofview.tactic val subst_gen : bool -> Names.Id.t list -> unit Proofview.tactic end @@ -5317,7 +5467,7 @@ sig val lemInv_clause : Misctypes.quantified_hypothesis -> EConstr.constr -> Names.Id.t list -> unit Proofview.tactic val add_inversion_lemma_exn : - Names.Id.t -> Constrexpr.constr_expr -> Misctypes.glob_sort -> bool -> (Names.Id.t -> unit Proofview.tactic) -> + Names.Id.t -> Constrexpr.constr_expr -> Sorts.family -> bool -> (Names.Id.t -> unit Proofview.tactic) -> unit end @@ -5394,19 +5544,21 @@ sig val add_hints : bool -> hint_db_name list -> hints_entry -> unit val searchtable_map : hint_db_name -> hint_db - val pp_hints_path_atom : ('a -> Pp.std_ppcmds) -> 'a hints_path_atom_gen -> Pp.std_ppcmds - val pp_hints_path_gen : ('a -> Pp.std_ppcmds) -> 'a hints_path_gen -> Pp.std_ppcmds + val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t + val pp_hints_path_gen : ('a -> Pp.t) -> 'a hints_path_gen -> Pp.t val glob_hints_path_atom : Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen - val pp_hints_path : hints_path -> Pp.std_ppcmds + val pp_hints_path : hints_path -> Pp.t val glob_hints_path : Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen + val run_hint : hint -> + ((raw_hint * Clenv.clausenv) hint_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic val typeclasses_db : hint_db_name val add_hints_init : (unit -> unit) -> unit val create_hint_db : bool -> hint_db_name -> Names.transparent_state -> bool -> unit val empty_hint_info : 'a Vernacexpr.hint_info_gen val repr_hint : hint -> (raw_hint * Clenv.clausenv) hint_ast - val pr_hint_db : Hint_db.t -> Pp.std_ppcmds + val pr_hint_db : Hint_db.t -> Pp.t end module Auto : @@ -5483,7 +5635,7 @@ sig val add_rew_rules : string -> raw_rew_rule list -> unit val find_rewrites : string -> rew_rule list val find_matches : string -> Constr.t -> rew_rule list - val print_rewrite_hintdb : string -> Pp.std_ppcmds + val print_rewrite_hintdb : string -> Pp.t end (************************************************************************) @@ -5496,8 +5648,8 @@ end module Ppvernac : sig - val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds - val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds + val pr_vernac : Vernacexpr.vernac_expr -> Pp.t + val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t end module Lemmas : @@ -5507,7 +5659,7 @@ sig val mk_hook : (Decl_kinds.locality -> Globnames.global_reference -> 'a) -> 'a declaration_hook - val start_proof : Names.Id.t -> ?pl:Proof_global.universe_binders -> Decl_kinds.goal_kind -> Evd.evar_map -> + val start_proof : Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind -> Evd.evar_map -> ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) -> ?sign:Environ.named_context_val -> EConstr.types -> ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> @@ -5520,14 +5672,14 @@ end module Himsg : sig - val explain_refiner_error : Logic.refiner_error -> Pp.std_ppcmds - val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.std_ppcmds + val explain_refiner_error : Logic.refiner_error -> Pp.t + val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.t end module ExplainErr : sig val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn - val register_additional_error_info : (Util.iexn -> Pp.std_ppcmds option Loc.located option) -> unit + val register_additional_error_info : (Util.iexn -> Pp.t option Loc.located option) -> unit end module Locality : @@ -5572,7 +5724,7 @@ sig val solve_all_obligations : unit Proofview.tactic option -> unit val admit_obligations : Names.Id.t option -> unit val show_obligations : ?msg:bool -> Names.Id.t option -> unit - val show_term : Names.Id.t option -> Pp.std_ppcmds + val show_term : Names.Id.t option -> Pp.t end module Command : @@ -5583,7 +5735,7 @@ sig type structured_fixpoint_expr = { fix_name : Id.t; - fix_univs : lident list option; + fix_univs : universe_decl_expr option; fix_annot : Id.t Loc.located option; fix_binders : local_binder_expr list; fix_body : constr_expr option; @@ -5592,7 +5744,7 @@ sig type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : lident list option; + ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } @@ -5608,7 +5760,7 @@ sig (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.lident list option -> + 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 @@ -5621,7 +5773,7 @@ sig val interp_fixpoint : structured_fixpoint_expr list -> Vernacexpr.decl_notation list -> - recursive_preentry * Vernacexpr.lident list option * UState.t * + recursive_preentry * Univdecls.universe_decl * UState.t * (EConstr.rel_context * Impargs.manual_implicits * int option) list val extract_mutual_inductive_declaration_components : @@ -5649,7 +5801,7 @@ sig ?refine:bool -> Decl_kinds.polymorphic -> Constrexpr.local_binder_expr list -> - Constrexpr.typeclass_constraint -> + Vernacexpr.typeclass_constraint -> (bool * Constrexpr.constr_expr) option -> ?generalize:bool -> ?tac:unit Proofview.tactic -> @@ -5686,6 +5838,16 @@ end module Vernacentries : sig + + type interp_state = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) + } + + val freeze_interp_state : Summary.marshallable -> interp_state + val unfreeze_interp_state : interp_state -> unit + val dump_global : Libnames.reference Misctypes.or_by_notation -> unit val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t @@ -5712,36 +5874,14 @@ end module Stm : sig - type state - val state_of_id : - Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] -end - -(************************************************************************) -(* End of modules from stm/ *) -(************************************************************************) + type doc -(************************************************************************) -(* Modules from highparsing/ *) -(************************************************************************) - -module G_vernac : -sig - - val def_body : Vernacexpr.definition_expr Pcoq.Gram.entry - val section_subset_expr : Vernacexpr.section_subset_expr Pcoq.Gram.entry - val query_command : (Vernacexpr.goal_selector option -> Vernacexpr.vernac_expr) Pcoq.Gram.entry - -end - -module G_proofs : -sig - - val hint : Vernacexpr.hints_expr Pcoq.Gram.entry - val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option + val get_doc : Feedback.doc_id -> doc + val state_of_id : doc:doc -> + Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] end (************************************************************************) -(* End of modules from highparsing/ *) +(* End of modules from stm/ *) (************************************************************************) |