aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml20
-rw-r--r--proofs/evar_refiner.mli2
-rw-r--r--proofs/goal.ml2
-rw-r--r--proofs/goal.mli2
-rw-r--r--proofs/logic.ml17
-rw-r--r--proofs/miscprint.ml7
-rw-r--r--proofs/pfedit.ml5
-rw-r--r--proofs/pfedit.mli10
-rw-r--r--proofs/proof.ml13
-rw-r--r--proofs/proof.mli62
-rw-r--r--proofs/proof_bullet.ml8
-rw-r--r--proofs/proof_bullet.mli10
-rw-r--r--proofs/proof_global.ml52
-rw-r--r--proofs/proof_global.mli23
-rw-r--r--proofs/refiner.mli4
-rw-r--r--proofs/tacmach.mli6
16 files changed, 127 insertions, 116 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5ef7fac814..16798a1d57 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -154,7 +154,7 @@ let error_incompatible_inst clenv mv =
Name id ->
user_err ~hdr:"clenv_assign"
(str "An incompatible instantiation has already been found for " ++
- pr_id id)
+ Id.print id)
| _ ->
anomaly ~label:"clenv_assign" (Pp.str "non dependent metavar already assigned.")
@@ -417,7 +417,7 @@ let check_bindings bl =
match List.duplicates qhyp_eq (List.map (fun x -> fst (snd x)) bl) with
| NamedHyp s :: _ ->
user_err
- (str "The variable " ++ pr_id s ++
+ (str "The variable " ++ Id.print s ++
str " occurs more than once in binding list.");
| AnonHyp n :: _ ->
user_err
@@ -435,12 +435,12 @@ let explain_no_such_bound_variable evd id =
in
let mvl = List.fold_left fold [] (Evd.meta_list evd) in
user_err ~hdr:"Evd.meta_with_name"
- (str"No such bound variable " ++ pr_id id ++
+ (str"No such bound variable " ++ Id.print id ++
(if mvl == [] then str " (no bound variables at all in the expression)."
else
(str" (possible name" ++
str (if List.length mvl == 1 then " is: " else "s are: ") ++
- pr_enum pr_id mvl ++ str").")))
+ pr_enum Id.print mvl ++ str").")))
let meta_with_name evd id =
let na = Name id in
@@ -460,7 +460,7 @@ let meta_with_name evd id =
n
| _ ->
user_err ~hdr:"Evd.meta_with_name"
- (str "Binder name \"" ++ pr_id id ++
+ (str "Binder name \"" ++ Id.print id ++
strbrk "\" occurs more than once in clause.")
let meta_of_binder clause loc mvs = function
@@ -474,7 +474,7 @@ let error_already_defined b =
match b with
| NamedHyp id ->
user_err
- (str "Binder name \"" ++ pr_id id ++
+ (str "Binder name \"" ++ Id.print id ++
str"\" already defined with incompatible value.")
| AnonHyp n ->
anomaly
@@ -639,10 +639,10 @@ let explain_no_such_bound_variable holes id =
let mvl = List.fold_right fold holes [] in
let expl = match mvl with
| [] -> str " (no bound variables at all in the expression)."
- | [id] -> str "(possible name is: " ++ pr_id id ++ str ")."
- | _ -> str "(possible names are: " ++ pr_enum pr_id mvl ++ str ")."
+ | [id] -> str "(possible name is: " ++ Id.print id ++ str ")."
+ | _ -> str "(possible names are: " ++ pr_enum Id.print mvl ++ str ")."
in
- user_err (str "No such bound variable " ++ pr_id id ++ expl)
+ user_err (str "No such bound variable " ++ Id.print id ++ expl)
let evar_with_name holes id =
let map h = match h.hole_name with
@@ -655,7 +655,7 @@ let evar_with_name holes id =
| [h] -> h.hole_evar
| _ ->
user_err
- (str "Binder name \"" ++ pr_id id ++
+ (str "Binder name \"" ++ Id.print id ++
str "\" occurs more than once in clause.")
let evar_of_binder holes = function
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index a0e3b718a2..d90cff5722 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -14,5 +14,5 @@ open Ltac_pretype
type glob_constr_ltac_closure = ltac_var_map * glob_constr
-val w_refine : evar * evar_info ->
+val w_refine : Evar.t * evar_info ->
glob_constr_ltac_closure -> evar_map -> evar_map
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 19f816a019..d5bc7e0ce2 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -16,7 +16,7 @@ module NamedDecl = Context.Named.Declaration
evar is defined in the current evar_map, should not be accessed. *)
(* type of the goals *)
-type goal = Evd.evar
+type goal = Evar.t
let pr_goal e = str "GOAL:" ++ Pp.int (Evar.repr e)
diff --git a/proofs/goal.mli b/proofs/goal.mli
index ad968cdfb3..37dd9d3c0c 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -58,7 +58,7 @@ module V82 : sig
(* Principal part of the progress tactical *)
val progress : goal list Evd.sigma -> goal Evd.sigma -> bool
-
+
(* Principal part of tclNOTSAMEGOAL *)
val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a633238f43..a9ad606a03 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -11,7 +11,6 @@ open CErrors
open Util
open Names
open Nameops
-open Term
open Constr
open Vars
open Termops
@@ -140,9 +139,9 @@ let reorder_context env sigma sign ord =
let ((d,h),mh) = find_q top moved_hyps in
if occur_vars_in_decl env sigma h d then
user_err ~hdr:"reorder_context"
- (str "Cannot move declaration " ++ pr_id top ++ spc() ++
+ (str "Cannot move declaration " ++ Id.print top ++ spc() ++
str "before " ++
- pr_sequence pr_id
+ pr_sequence Id.print
(Id.Set.elements (Id.Set.inter h
(global_vars_set_of_decl env sigma d))));
step ord' expected ctxt_head mh (d::ctxt_tail)
@@ -173,7 +172,7 @@ let check_decl_position env sigma sign d =
let deps = dependency_closure env sigma (named_context_of_val sign) needed in
if Id.List.mem x deps then
user_err ~hdr:"Logic.check_decl_position"
- (str "Cannot create self-referring hypothesis " ++ pr_id x);
+ (str "Cannot create self-referring hypothesis " ++ Id.print x);
x::deps
(* Auxiliary functions for primitive MOVE tactic
@@ -234,10 +233,10 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
if not (move_location_eq hto (MoveAfter hyp)) then
(first, d::middle)
else
- user_err ~hdr:"move_hyp" (str "Cannot move " ++ pr_id (NamedDecl.get_id declfrom) ++
- Miscprint.pr_move_location pr_id hto ++
+ user_err ~hdr:"move_hyp" (str "Cannot move " ++ Id.print (NamedDecl.get_id declfrom) ++
+ Miscprint.pr_move_location Id.print hto ++
str (if toleft then ": it occurs in the type of " else ": it depends on ")
- ++ pr_id hyp ++ str ".")
+ ++ Id.print hyp ++ str ".")
else
(d::first, middle)
in
@@ -507,10 +506,10 @@ let convert_hyp check sign sigma d =
let env = Global.env_of_context sign in
if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then
user_err ~hdr:"Logic.convert_hyp"
- (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
+ (str "Incorrect change of the type of " ++ Id.print id ++ str ".");
if check && not (Option.equal (is_conv env sigma) b c) then
user_err ~hdr:"Logic.convert_hyp"
- (str "Incorrect change of the body of "++ pr_id id ++ str ".");
+ (str "Incorrect change of the body of "++ Id.print id ++ str ".");
if check then reorder := check_decl_position env sigma sign d;
map_named_decl EConstr.Unsafe.to_constr d) in
reorder_val_context env sigma sign' !reorder
diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml
index 5d37c8a024..92b58b4092 100644
--- a/proofs/miscprint.ml
+++ b/proofs/miscprint.ml
@@ -6,8 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Misctypes
open Pp
+open Names
+open Misctypes
(** Printing of [intro_pattern] *)
@@ -18,8 +19,8 @@ let rec pr_intro_pattern prc (_,pat) = match pat with
| IntroAction p -> pr_intro_pattern_action prc p
and pr_intro_pattern_naming = function
- | IntroIdentifier id -> Nameops.pr_id id
- | IntroFresh id -> str "?" ++ Nameops.pr_id id
+ | IntroIdentifier id -> Id.print id
+ | IntroFresh id -> str "?" ++ Id.print id
| IntroAnonymous -> str "?"
and pr_intro_pattern_action prc = function
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 2d4aba17cb..c526ae000a 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -51,9 +51,8 @@ end
let get_nth_V82_goal i =
let p = Proof_global.give_me_the_proof () in
- let { it=goals ; sigma = sigma; } = Proof.V82.subgoals p in
- try
- { it=(List.nth goals (i-1)) ; sigma=sigma; }
+ let goals,_,_,_,sigma = Proof.proof p in
+ try { it = List.nth goals (i-1) ; sigma }
with Failure _ -> raise NoSuchGoal
let get_goal_context_gen i =
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 21a65f8eb6..2acb678d7f 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -74,7 +74,7 @@ val current_proof_statement :
val solve : ?with_end_tac:unit Proofview.tactic ->
Vernacexpr.goal_selector -> int option -> unit Proofview.tactic ->
- Proof.proof -> Proof.proof*bool
+ Proof.t -> Proof.t * bool
(** [by tac] applies tactic [tac] to the 1st subgoal of the current
focused proof or raises a UserError if there is no focused proof or
@@ -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 ba4980b66b..04e707cd66 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -98,7 +98,7 @@ let done_cond ?(loose_end=false) k = CondDone (loose_end,k)
(* Subpart of the type of proofs. It contains the parts of the proof which
are under control of the undo mechanism *)
-type proof = {
+type t = {
(* Current focused proofview *)
proofview: Proofview.proofview;
(* Entry for the proofview *)
@@ -112,9 +112,11 @@ 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
}
+type proof = t
+
(*** General proof functions ***)
let proof p =
@@ -163,6 +165,7 @@ let map_structured_proof pfts process_goal: 'a pre_goals =
let rec unroll_focus pv = function
| (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
| [] -> pv
+
(* spiwack: a proof is considered completed even if its still focused, if the focus
doesn't hide any goal.
Unfocusing is handled in {!return}. *)
@@ -391,10 +394,12 @@ let pr_proof p =
(*** Compatibility layer with <=v8.2 ***)
module V82 = struct
let subgoals p =
- Proofview.V82.goals p.proofview
+ let it, sigma = Proofview.proofview p.proofview in
+ Evd.{ it; sigma }
let background_subgoals p =
- Proofview.V82.goals (unroll_focus p.proofview p.focus_stack)
+ let it, sigma = Proofview.proofview (unroll_focus p.proofview p.focus_stack) in
+ Evd.{ it; sigma }
let top_goal p =
let { Evd.it=gls ; sigma=sigma; } =
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 698aa48b02..0b5e771ef3 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -30,7 +30,9 @@
*)
(* Type of a proof. *)
-type proof
+type t
+type proof = t
+[@@ocaml.deprecated "please use [Proof.t]"]
(* Returns a stylised view of a proof for use by, for instance,
ide-s. *)
@@ -42,7 +44,7 @@ type proof
shelf (the list of goals on the shelf), a representation of the
given up goals (the list of the given up goals) and the underlying
evar_map *)
-val proof : proof ->
+val proof : t ->
Goal.goal list
* (Goal.goal list * Goal.goal list) list
* Goal.goal list
@@ -61,27 +63,26 @@ type 'a pre_goals = {
(** List of the goals that have been given up *)
}
-val map_structured_proof : proof -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals)
+val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals)
(*** General proof functions ***)
-
-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 start : Evd.evar_map -> (Environ.env * EConstr.types) list -> t
+val dependent_start : Proofview.telescope -> t
+val initial_goals : t -> (EConstr.constr * EConstr.types) list
+val initial_euctx : t -> 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). *)
-val is_done : proof -> bool
+val is_done : t -> bool
(* Like is_done, but this time it really means done (i.e. nothing left to do) *)
-val is_complete : proof -> bool
+val is_complete : t -> bool
(* Returns the list of partial proofs to initial goals. *)
-val partial_proof : proof -> EConstr.constr list
+val partial_proof : t -> EConstr.constr list
-val compact : proof -> proof
+val compact : t -> t
(* Returns the proofs (with their type) of the initial goals.
Raises [UnfinishedProof] is some goals remain to be considered.
@@ -92,7 +93,7 @@ exception UnfinishedProof
exception HasShelvedGoals
exception HasGivenUpGoals
exception HasUnresolvedEvar
-val return : proof -> Evd.evar_map
+val return : t -> Evd.evar_map
(*** Focusing actions ***)
@@ -132,7 +133,7 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
(* focus command (focuses on the [i]th subgoal) *)
(* spiwack: there could also, easily be a focus-on-a-range tactic, is there
a need for it? *)
-val focus : 'a focus_condition -> 'a -> int -> proof -> proof
+val focus : 'a focus_condition -> 'a -> int -> t -> t
exception FullyUnfocused
exception CannotUnfocusThisWay
@@ -148,58 +149,59 @@ exception NoSuchGoals of int * int
Raises [FullyUnfocused] if the proof is not focused.
Raises [CannotUnfocusThisWay] if the proof the unfocusing condition
is not met. *)
-val unfocus : 'a focus_kind -> proof -> unit -> proof
+val unfocus : 'a focus_kind -> t -> unit -> t
(* [unfocused p] returns [true] when [p] is fully unfocused. *)
-val unfocused : proof -> bool
+val unfocused : t -> bool
(* [get_at_focus k] gets the information stored at the closest focus point
of kind [k].
Raises [NoSuchFocus] if there is no focus point of kind [k]. *)
exception NoSuchFocus
-val get_at_focus : 'a focus_kind -> proof -> 'a
+val get_at_focus : 'a focus_kind -> t -> 'a
(* [is_last_focus k] check if the most recent focus is of kind [k] *)
-val is_last_focus : 'a focus_kind -> proof -> bool
+val is_last_focus : 'a focus_kind -> t -> bool
(* returns [true] if there is no goal under focus. *)
-val no_focused_goal : proof -> bool
+val no_focused_goal : t -> bool
(*** Tactics ***)
(* the returned boolean signal whether an unsafe tactic has been
used. In which case it is [false]. *)
val run_tactic : Environ.env ->
- unit Proofview.tactic -> proof -> proof*(bool*Proofview_monad.Info.tree)
+ unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree)
-val maximal_unfocus : 'a focus_kind -> proof -> proof
+val maximal_unfocus : 'a focus_kind -> t -> t
(*** Commands ***)
-val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a
+val in_proof : t -> (Evd.evar_map -> 'a) -> 'a
(* Remove all the goals from the shelf and adds them at the end of the
focused goals. *)
-val unshelve : proof -> proof
+val unshelve : t -> t
-val pr_proof : proof -> Pp.t
+val pr_proof : t -> Pp.t
(*** Compatibility layer with <=v8.2 ***)
module V82 : sig
- val subgoals : proof -> Goal.goal list Evd.sigma
+ val subgoals : t -> Goal.goal list Evd.sigma
+ [@@ocaml.deprecated "Use the first and fifth argument of [Proof.proof]"]
(* All the subgoals of the proof, including those which are not focused. *)
- val background_subgoals : proof -> Goal.goal list Evd.sigma
+ val background_subgoals : t -> Goal.goal list Evd.sigma
- val top_goal : proof -> Goal.goal Evd.sigma
+ val top_goal : t -> Goal.goal Evd.sigma
(* returns the existential variable used to start the proof *)
- val top_evars : proof -> Evd.evar list
+ val top_evars : t -> Evar.t list
(* Turns the unresolved evars into goals.
Raises [UnfinishedProof] if there are still unsolved goals. *)
- val grab_evars : proof -> proof
+ val grab_evars : t -> t
(* Implements the Existential command *)
- val instantiate_evar : int -> Constrexpr.constr_expr -> proof -> proof
+ val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t
end
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index 4f575ab4be..2149163314 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -25,8 +25,8 @@ let pr_bullet b =
type behavior = {
name : string;
- put : proof -> t -> proof;
- suggest: proof -> Pp.t
+ put : Proof.t -> t -> Proof.t;
+ suggest: Proof.t -> Pp.t
}
let behaviors = Hashtbl.create 4
@@ -110,7 +110,7 @@ module Strict = struct
let push (b:t) pr =
focus bullet_cond (b::get_bullets pr) 1 pr
- let suggest_bullet (prf : proof): suggestion =
+ let suggest_bullet (prf : Proof.t): suggestion =
if is_done prf then ProofFinished
else if not (no_focused_goal prf)
then (* No suggestion if a bullet is not mandatory, look for an unfinished bullet *)
@@ -137,7 +137,7 @@ module Strict = struct
in
loop prf
- let rec pop_until (prf : proof) bul : proof =
+ let rec pop_until (prf : Proof.t) bul : Proof.t =
let prf', b = pop prf in
if bullet_eq bul b then prf'
else pop_until prf' bul
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index 9e924fec97..09fcabf50a 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -12,8 +12,6 @@
(* *)
(**********************************************************)
-open Proof
-
type t = Vernacexpr.bullet
(** A [behavior] is the data of a put function which
@@ -22,8 +20,8 @@ type t = Vernacexpr.bullet
with a name to identify the behavior. *)
type behavior = {
name : string;
- put : proof -> t -> proof;
- suggest: proof -> Pp.t
+ put : Proof.t -> t -> Proof.t;
+ suggest: Proof.t -> Pp.t
}
(** A registered behavior can then be accessed in Coq
@@ -39,8 +37,8 @@ val register_behavior : behavior -> unit
(** Handles focusing/defocusing with bullets:
*)
-val put : proof -> t -> proof
-val suggest : proof -> Pp.t
+val put : Proof.t -> t -> Proof.t
+val suggest : Proof.t -> Pp.t
(**********************************************************)
(* *)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 97faa16848..c1e1c2edad 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;
@@ -90,12 +90,15 @@ type pstate = {
terminator : proof_terminator CEphemeron.key;
endline_tactic : Genarg.glob_generic_argument option;
section_vars : Context.Named.t option;
- proof : Proof.proof;
+ proof : Proof.t;
strength : Decl_kinds.goal_kind;
mode : proof_mode CEphemeron.key;
universe_decl: Univdecls.universe_decl;
}
+type t = pstate list
+type state = t
+
let make_terminator f = f
let apply_terminator f = f
@@ -185,7 +188,7 @@ let msg_proofs () =
match get_all_proof_names () with
| [] -> (spc () ++ str"(No proof-editing in progress).")
| l -> (str"." ++ fnl () ++ str"Proofs currently edited:" ++ spc () ++
- (pr_sequence Nameops.pr_id l) ++ str".")
+ (pr_sequence Id.print l) ++ str".")
let there_is_a_proof () = not (List.is_empty !pstates)
let there_are_pending_proofs () = there_is_a_proof ()
@@ -316,11 +319,7 @@ let get_open_goals () =
(List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
List.length shelf
-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) =
@@ -329,10 +328,12 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
let poly = pi2 strength (* Polymorphic *) in
let initial_goals = Proof.initial_goals proof in
let initial_euctx = Proof.initial_euctx proof in
+ let constrain_variables ctx =
+ UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
+ in
let fpl, univs = Future.split2 fpl in
let universes = if poly || now then Future.force univs else initial_euctx in
- let binders, univctx = Evd.check_univ_decl (Evd.from_ctx universes) universe_decl in
- let binders = if poly then Some binders else None in
+ let binders = if poly then Some (UState.universe_binders universes) else None in
(* Because of dependent subgoals at the beginning of proofs, we could
have existential variables in the initial types of goals, we need to
normalise them for the kernel. *)
@@ -348,20 +349,25 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then
nf t
else t
- in
+ in
let used_univs_body = Univops.universes_of_constr body in
let used_univs_typ = Univops.universes_of_constr typ in
+ (* Universes for private constants are relevant to the body *)
+ let used_univs_body =
+ List.fold_left (fun acc (us,_) -> Univ.LSet.union acc us)
+ used_univs_body (Safe_typing.universes_of_private eff)
+ in
if keep_body_ucst_separate ||
not (Safe_typing.empty_private_constants = eff) then
- let initunivs = Evd.evar_context_universe_context initial_euctx in
- let ctx = constrain_variables initunivs universes in
+ let initunivs = UState.const_univ_entry ~poly initial_euctx in
+ let ctx = constrain_variables universes in
(* For vi2vo compilation proofs are computed now but we need to
complement the univ constraints of the typ with the ones of
the body. So we keep the two sets distinct. *)
let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
let ctx_body = UState.restrict ctx used_univs in
- let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx_body) universe_decl in
- (initunivs, typ), ((body, Univ.ContextSet.of_context univs), eff)
+ let univs = UState.check_mono_univ_decl ctx_body universe_decl in
+ (initunivs, typ), ((body, univs), eff)
else
(* Since the proof is computed now, we can simply have 1 set of
constraints in which we merge the ones for the body and the ones
@@ -370,30 +376,28 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
TODO: check if restrict is really necessary now. *)
let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
let ctx = UState.restrict universes used_univs in
- let _, univs = Evd.check_univ_decl (Evd.from_ctx ctx) universe_decl in
+ let univs = UState.check_univ_decl ~poly ctx universe_decl in
(univs, typ), ((body, Univ.ContextSet.empty), eff)
in
fun t p -> Future.split2 (Future.chain p (make_body t))
else
fun t p ->
+ (* Already checked the univ_decl for the type universes when starting the proof. *)
+ let univctx = Entries.Monomorphic_const_entry (UState.context_set universes) in
Future.from_val (univctx, nf t),
Future.chain p (fun (pt,eff) ->
(* Deferred proof, we already checked the universe declaration with
the initial universes, ensure that the final universes respect
the declaration as well. If the declaration is non-extensible,
this will prevent the body from adding universes and constraints. *)
- let bodyunivs = constrain_variables univctx (Future.force univs) in
- let _, univs = Evd.check_univ_decl (Evd.from_ctx bodyunivs) universe_decl in
- (pt,Univ.ContextSet.of_context univs),eff)
+ let bodyunivs = constrain_variables (Future.force univs) in
+ let univs = UState.check_mono_univ_decl bodyunivs universe_decl in
+ (pt,univs),eff)
in
let entry_fn p (_, t) =
let t = EConstr.Unsafe.to_constr t in
let univstyp, body = make_body t p in
let univs, typ = Future.force univstyp in
- let univs =
- if poly then Entries.Polymorphic_const_entry univs
- else Entries.Monomorphic_const_entry univs
- in
{Entries.
const_entry_body = body;
const_entry_secctx = section_vars;
@@ -466,8 +470,6 @@ module V82 = struct
pid, (goals, strength)
end
-type state = pstate list
-
let freeze ~marshallable =
match marshallable with
| `Yes ->
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 6309f681f8..059459042b 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -10,6 +10,10 @@
toplevel. In particular it defines the global proof
environment. *)
+type t
+type state = t
+[@@ocaml.deprecated "please use [Proof_global.t]"]
+
val there_are_pending_proofs : unit -> bool
val check_no_pending_proof : unit -> unit
@@ -21,7 +25,7 @@ val discard_current : unit -> unit
val discard_all : unit -> unit
exception NoCurrentProof
-val give_me_the_proof : unit -> Proof.proof
+val give_me_the_proof : unit -> Proof.t
(** @raise NoCurrentProof when outside proof mode. *)
val compact_the_proof : unit -> unit
@@ -33,7 +37,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 +90,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. *)
@@ -107,9 +111,9 @@ val get_open_goals : unit -> int
no current proof.
The return boolean is set to [false] if an unsafe tactic has been used. *)
val with_current_proof :
- (unit Proofview.tactic -> Proof.proof -> Proof.proof*'a) -> 'a
+ (unit Proofview.tactic -> Proof.t -> Proof.t * 'a) -> 'a
val simple_with_current_proof :
- (unit Proofview.tactic -> Proof.proof -> Proof.proof) -> unit
+ (unit Proofview.tactic -> Proof.t -> Proof.t) -> unit
(** Sets the tactic to be used when a tactic line is closed with [...] *)
val set_endline_tactic : Genarg.glob_generic_argument -> unit
@@ -129,11 +133,10 @@ module V82 : sig
Decl_kinds.goal_kind)
end
-type state
-val freeze : marshallable:[`Yes | `No | `Shallow] -> state
-val unfreeze : state -> unit
-val proof_of_state : state -> Proof.proof
-val copy_terminators : src:state -> tgt:state -> state
+val freeze : marshallable:[`Yes | `No | `Shallow] -> t
+val unfreeze : t -> unit
+val proof_of_state : t -> Proof.t
+val copy_terminators : src:t -> tgt:t -> t
(**********************************************************)
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 9c8777c413..34e517aedc 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 6441cfd195..d9496d2b4f 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 21:49:36 +0000