diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 61 | ||||
| -rw-r--r-- | API/grammar_API.mli | 3 |
2 files changed, 38 insertions, 26 deletions
diff --git a/API/API.mli b/API/API.mli index 20a637c1fa..69278e7c9f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2055,8 +2055,10 @@ sig type explicitation = Constrexpr.explicitation = | ExplByPos of int * Names.Id.t option | ExplByName of Names.Id.t + type sign = bool + type raw_natural_number = string type prim_token = Constrexpr.prim_token = - | Numeral of Bigint.bigint + | Numeral of raw_natural_number * sign | String of string type notation = string type instance_expr = Misctypes.glob_level list @@ -2556,6 +2558,20 @@ sig and closed_glob_constr = Glob_term.closed_glob_constr = { closure: closure; term: glob_constr } + + type var_map = Pattern.constr_under_binders Names.Id.Map.t + type uconstr_var_map = Glob_term.closed_glob_constr Names.Id.Map.t + type unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.t + type ltac_var_map = Glob_term.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 *) + } end module Libnames : @@ -2680,7 +2696,6 @@ module Lib : sig | ClosedModule of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen | ClosedSection of library_segment - | FrozenState of Summary.frozen and library_segment = (Libnames.object_name * node) list @@ -2921,10 +2936,6 @@ sig | IsType | WithoutTypeConstraint - type var_map = Pattern.constr_under_binders Names.Id.Map.t - type uconstr_var_map = Glob_term.closed_glob_constr Names.Id.Map.t - type unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.t - type inference_hook = Environ.env -> Evd.evar_map -> Evar.t -> Evd.evar_map * EConstr.constr type inference_flags = Pretyping.inference_flags = { use_typeclasses : bool; @@ -2934,22 +2945,11 @@ sig expand_evars : bool } - type ltac_var_map = Pretyping.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 *) - } type pure_open_constr = Evd.evar_map * EConstr.constr - type glob_constr_ltac_closure = ltac_var_map * Glob_term.glob_constr + type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr - val empty_lvar : ltac_var_map val understand_ltac : inference_flags -> - Environ.env -> Evd.evar_map -> ltac_var_map -> + Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> pure_open_constr val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map -> ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr @@ -2963,11 +2963,11 @@ sig val interp_elimination_sort : Misctypes.glob_sort -> Sorts.family val register_constr_interp0 : ('r, 'g, 't) Genarg.genarg_type -> - (unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit + (Glob_term.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 -> - ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr + Glob_term.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr end module Evarconv : @@ -3307,6 +3307,7 @@ sig val declare_cache_obj : (unit -> unit) -> string -> unit val add_known_plugin : (unit -> unit) -> string -> unit val add_known_module : string -> unit + val module_is_known : string -> bool end (* All items in the Proof_type module are deprecated. *) @@ -3465,6 +3466,8 @@ sig (** @raise NoCurrentProof when outside proof mode. *) val discard_all : unit -> unit + val discard_current : unit -> unit + val get_current_proof_name : unit -> Names.Id.t end module Nametab : @@ -3795,6 +3798,7 @@ sig val cases_pattern_of_glob_constr : Names.Name.t -> Glob_term.glob_constr -> Glob_term.cases_pattern 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 end module Indrec : @@ -3939,11 +3943,18 @@ sig val solve : ?with_end_tac:unit Proofview.tactic -> Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> Proof.proof -> Proof.proof * bool - val delete_current_proof : unit -> unit val cook_proof : unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind)) - val get_current_proof_name : unit -> Names.Id.t + val get_current_context : unit -> Evd.evar_map * Environ.env + + (* Deprecated *) + val delete_current_proof : unit -> unit + [@@ocaml.deprecated "use Proof_global.discard_current"] + + val get_current_proof_name : unit -> Names.Id.t + [@@ocaml.deprecated "use Proof_global.get_current_proof_name"] + end module Tactics : @@ -4100,7 +4111,7 @@ sig module New : sig - val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic + val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic val reduce_after_refine : unit Proofview.tactic end module Simple : @@ -4490,7 +4501,7 @@ end module Refine : sig - val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit Proofview.tactic + val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit Proofview.tactic val solve_constraints : unit Proofview.tactic end diff --git a/API/grammar_API.mli b/API/grammar_API.mli index 44aae771f6..c643f09086 100644 --- a/API/grammar_API.mli +++ b/API/grammar_API.mli @@ -116,7 +116,7 @@ sig val pattern_identref : Names.Id.t located Gram.Entry.e val base_ident : Names.Id.t Gram.Entry.e val natural : int Gram.Entry.e - val bigint : Bigint.bigint Gram.Entry.e + val bigint : Constrexpr.raw_natural_number Gram.Entry.e val integer : int Gram.Entry.e val string : string Gram.Entry.e val qualid : API.Libnames.qualid located Gram.Entry.e @@ -211,6 +211,7 @@ end module Mltop : sig val add_known_module : string -> unit + val module_is_known : string -> bool val declare_cache_obj : (unit -> unit) -> string -> unit end module Vernacinterp : |