diff options
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.ml | 1 | ||||
| -rw-r--r-- | API/API.mli | 72 |
2 files changed, 57 insertions, 16 deletions
diff --git a/API/API.ml b/API/API.ml index f588fe193a..78d9c0c26e 100644 --- a/API/API.ml +++ b/API/API.ml @@ -275,6 +275,7 @@ module Command = Command module Classes = Classes (* module Record *) (* module Assumptions *) +module Vernacstate = Vernacstate module Vernacinterp = Vernacinterp module Mltop = Mltop module Topfmt = Topfmt diff --git a/API/API.mli b/API/API.mli index 704f1a3569..86c6f14158 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4389,6 +4389,8 @@ sig val default_binder_kind : Constrexpr.binder_kind val mkLetInC : Names.Name.t Loc.located * Constrexpr.constr_expr * Constrexpr.constr_expr option * Constrexpr.constr_expr -> Constrexpr.constr_expr val mkCProdN : ?loc:Loc.t -> Constrexpr.local_binder_expr list -> Constrexpr.constr_expr -> Constrexpr.constr_expr + val replace_vars_constr_expr : + Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr end module Notation_ops : @@ -4443,8 +4445,11 @@ end module Topconstr : sig + val replace_vars_constr_expr : - Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr + Names.Id.t Names.Id.Map.t -> Constrexpr.constr_expr -> Constrexpr.constr_expr + [@@ocaml.deprecated "use Constrexpr_ops.free_vars_of_constr_expr"] + end module Constrintern : @@ -4645,16 +4650,23 @@ sig type proof type 'a focus_kind + val proof : proof -> + Goal.goal list * (Goal.goal list * Goal.goal list) list * + Goal.goal list * Goal.goal list * Evd.evar_map + val run_tactic : Environ.env -> unit Proofview.tactic -> proof -> proof * (bool * Proofview_monad.Info.tree) val unshelve : proof -> proof val maximal_unfocus : 'a focus_kind -> proof -> proof val pr_proof : proof -> Pp.t + module V82 : sig val grab_evars : proof -> proof val subgoals : proof -> Goal.goal list Evd.sigma + [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"] + end end @@ -5138,12 +5150,20 @@ sig val pr_lconstr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.t val pr_constr : Constr.t -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lconstr : Constr.t -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_econstr : EConstr.constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_glob_constr : Glob_term.glob_constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_constr_pattern : Pattern.constr_pattern -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + 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_n_env : Environ.env -> Evd.evar_map -> Notation_term.tolerability -> EConstr.constr -> Pp.t @@ -5151,11 +5171,17 @@ sig 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 + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_lglob_constr : Glob_term.glob_constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val pr_leconstr : EConstr.constr -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_global : Globnames.global_reference -> Pp.t val pr_lconstr_under_binders : Ltac_pretype.constr_under_binders -> Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + 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 @@ -5164,7 +5190,11 @@ sig 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 + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t + [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"] + 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 @@ -5677,7 +5707,9 @@ sig 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_env : Environ.env -> Evd.evar_map -> Hint_db.t -> Pp.t val pr_hint_db : Hint_db.t -> Pp.t + [@@ocaml.deprecated "please used pr_hint_db_env"] end module Auto : @@ -5754,7 +5786,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.t + val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t end (************************************************************************) @@ -5787,11 +5819,12 @@ sig Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> Globnames.global_reference -> 'a val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit val get_current_context : unit -> Evd.evar_map * Environ.env + [@@ocaml.deprecated "please use [Pfedit.get_current_context]"] end module Himsg : sig - val explain_refiner_error : Logic.refiner_error -> Pp.t + val explain_refiner_error : Environ.env -> Evd.evar_map -> Logic.refiner_error -> Pp.t val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.t end @@ -5929,14 +5962,30 @@ sig Names.Id.t end +module Vernacstate : +sig + + type t = { (* 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) *) + } + + (* XXX: This should not be exported *) + val freeze_interp_state : Summary.marshallable -> t + val unfreeze_interp_state : t -> unit + +end + module Vernacinterp : sig + type deprecation = bool - type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit + type vernac_command = + Genarg.raw_generic_argument list -> Loc.t option -> Vernacstate.t -> Vernacstate.t - val vinterp_add : deprecation -> Vernacexpr.extend_name -> - vernac_command -> unit + val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit end @@ -5958,15 +6007,6 @@ 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 @@ -5998,7 +6038,7 @@ sig 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 ] + Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ] end (************************************************************************) |