diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.ml | 18 | ||||
| -rw-r--r-- | API/API.mli | 492 |
2 files changed, 260 insertions, 250 deletions
diff --git a/API/API.ml b/API/API.ml index c952e123d4..68da858ba0 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 @@ -169,7 +169,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 *) @@ -224,6 +223,9 @@ module Pcoq = Pcoq module Egramml = Egramml (* Egramcoq *) +module G_vernac = G_vernac +module G_proofs = G_proofs + (******************************************************************************) (* Tactics *) (******************************************************************************) @@ -277,9 +279,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..901ed3528b 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 @@ -1750,10 +1756,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 +1768,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,7 +1784,7 @@ 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 dirpath : full_path -> Names.DirPath.t @@ -1788,7 +1794,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 +1806,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 @@ -1930,7 +1936,7 @@ sig 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 pr_global_env : Names.Id.Set.t -> Globnames.global_reference -> Pp.t val shortest_qualid_of_tactic : Names.KerName.t -> Libnames.qualid val basename_of_global : Globnames.global_reference -> Names.Id.t @@ -2053,7 +2059,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 +2112,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 +2135,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 @@ -2753,9 +2760,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 +2807,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 +2831,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 +2914,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 +3047,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,55 +3081,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 'a tomatch_tuple_g = ('a glob_constr_g * 'a predicate_pattern_g) + + and 'a tomatch_tuples_g = 'a tomatch_tuple_g list - and tomatch_tuples = tomatch_tuple 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 - and cases_clause = (Names.Id.t list * cases_pattern list * glob_constr) Loc.located - and cases_clauses = cases_clause 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 (** A globalised term together with a closure representing the value of its free variables. Intended for use when these variables are taken @@ -3183,6 +3205,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 : @@ -3290,16 +3316,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 @@ -3781,6 +3807,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 +3820,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 @@ -3805,7 +3837,7 @@ sig | 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 + | 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 @@ -3964,16 +3996,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.t list -> 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,22 +4041,14 @@ 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 + 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 @@ -4117,6 +4144,7 @@ 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 @@ -4172,22 +4200,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 +4215,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 +4300,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 +4352,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 +4372,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 +4404,16 @@ end module Evar_refiner : sig + type glob_constr_ltac_closure = Glob_term.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 +4449,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 @@ -4510,13 +4528,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 +4593,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 @@ -4626,6 +4644,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 +4667,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 +4706,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 +4776,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 +4853,23 @@ 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 + val hint_proof_using : 'a Pcoq.Gram.entry -> 'a option -> 'a option + +end + (************************************************************************) (* End of modules from parsing/ *) (************************************************************************) @@ -4843,7 +4880,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 +4888,74 @@ 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 : Glob_term.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 : Pattern.constr_under_binders -> Pp.t + val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.t + + val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.t + val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Glob_term.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 (************************************************************************) @@ -4936,7 +4973,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 +5010,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 +5072,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 : @@ -5233,7 +5270,7 @@ sig 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 -> @@ -5317,7 +5354,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 +5431,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 +5522,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 +5535,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 : @@ -5520,14 +5559,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 +5611,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 : @@ -5720,28 +5759,3 @@ end (************************************************************************) (* End of modules from stm/ *) (************************************************************************) - -(************************************************************************) -(* 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 - -end - -(************************************************************************) -(* End of modules from highparsing/ *) -(************************************************************************) |