From ed0c434a05a929a659e43aed80ab7c8179a7daa3 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 13 Nov 2017 19:03:03 +0100 Subject: [api] Insert miscellaneous API deprecation back to core. --- proofs/pfedit.mli | 8 ++++---- proofs/proof.ml | 2 +- proofs/proof.mli | 2 +- proofs/proof_global.ml | 4 ++-- proofs/proof_global.mli | 4 ++-- proofs/refiner.mli | 4 ++-- proofs/tacmach.mli | 6 ++++-- 7 files changed, 16 insertions(+), 14 deletions(-) (limited to 'proofs') diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 21a65f8eb..d676a0874 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -95,14 +95,14 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit tactic. *) val build_constant_by_tactic : - Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind -> + Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind -> EConstr.types -> unit Proofview.tactic -> Safe_typing.private_constants Entries.definition_entry * bool * - Evd.evar_universe_context + UState.t -val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> +val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic -> EConstr.types -> unit Proofview.tactic -> - constr * bool * Evd.evar_universe_context + constr * bool * UState.t val refine_by_tactic : env -> Evd.evar_map -> EConstr.types -> unit Proofview.tactic -> constr * Evd.evar_map diff --git a/proofs/proof.ml b/proofs/proof.ml index ba4980b66..e24d57f08 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -112,7 +112,7 @@ type proof = { (* List of goals that have been given up *) given_up : Goal.goal list; (* The initial universe context (for the statement) *) - initial_euctx : Evd.evar_universe_context + initial_euctx : UState.t } (*** General proof functions ***) diff --git a/proofs/proof.mli b/proofs/proof.mli index 698aa48b0..48aed8225 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -69,7 +69,7 @@ val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre val start : Evd.evar_map -> (Environ.env * EConstr.types) list -> proof val dependent_start : Proofview.telescope -> proof val initial_goals : proof -> (EConstr.constr * EConstr.types) list -val initial_euctx : proof -> Evd.evar_universe_context +val initial_euctx : proof -> UState.t (* Returns [true] if the considered proof is completed, that is if no goal remain to be considered (this does not require that all evars have been solved). *) diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 8b788bb38..fdc9a236b 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -68,7 +68,7 @@ let _ = (* Extra info on proofs. *) type lemma_possible_guards = int list list -type proof_universes = Evd.evar_universe_context * Universes.universe_binders option +type proof_universes = UState.t * Universes.universe_binders option type proof_object = { id : Names.Id.t; @@ -320,7 +320,7 @@ let constrain_variables init uctx = let levels = Univ.Instance.levels (Univ.UContext.instance init) in UState.constrain_variables levels uctx -type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * Evd.evar_universe_context +type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t let close_proof ~keep_body_ucst_separate ?feedback_id ~now (fpl : closed_proof_output Future.computation) = diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 6309f681f..eed62f912 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -33,7 +33,7 @@ val compact_the_proof : unit -> unit (i.e. an proof ending command) and registers the appropriate values. *) type lemma_possible_guards = int list list -type proof_universes = Evd.evar_universe_context * Universes.universe_binders option +type proof_universes = UState.t * Universes.universe_binders option type proof_object = { id : Names.Id.t; @@ -86,7 +86,7 @@ val close_proof : keep_body_ucst_separate:bool -> Future.fix_exn -> closed_proof * Both access the current proof state. The former is supposed to be * chained with a computation that completed the proof *) -type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * Evd.evar_universe_context +type closed_proof_output = (Constr.t * Safe_typing.private_constants) list * UState.t (* If allow_partial is set (default no) then an incomplete proof * is allowed (no error), and a warn is given if the proof is complete. *) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 9c8777c41..34e517aed 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -35,10 +35,10 @@ val tclIDTAC_MESSAGE : Pp.t -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic -val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic +val tclEVARUNIVCONTEXT : UState.t -> tactic val tclPUSHCONTEXT : Evd.rigid -> Univ.ContextSet.t -> tactic -> tactic -val tclPUSHEVARUNIVCONTEXT : Evd.evar_universe_context -> tactic +val tclPUSHEVARUNIVCONTEXT : UState.t -> tactic val tclPUSHCONSTRAINTS : Univ.constraints -> tactic diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 6441cfd19..d9496d2b4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -10,7 +10,6 @@ open Names open Constr open Environ open EConstr -open Evd open Proof_type open Redexpr open Pattern @@ -19,7 +18,10 @@ open Ltac_pretype (** Operations for handling terms under a local typing context. *) -type 'a sigma = 'a Evd.sigma;; +type 'a sigma = 'a Evd.sigma +[@@ocaml.deprecated "alias of Evd.sigma"] + +open Evd type tactic = Proof_type.tactic;; val sig_it : 'a sigma -> 'a -- cgit v1.2.3