aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/clenv.ml2
-rw-r--r--proofs/clenvtac.ml2
-rw-r--r--proofs/logic.ml2
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--proofs/proof_global.ml19
-rw-r--r--proofs/proof_global.mli10
-rw-r--r--proofs/redexpr.ml8
-rw-r--r--proofs/refine.ml23
-rw-r--r--proofs/refiner.mli3
-rw-r--r--proofs/tacmach.ml4
-rw-r--r--proofs/tacmach.mli3
11 files changed, 38 insertions, 40 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index aeaf16723b..450fcddfde 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -13,8 +13,8 @@ open CErrors
open Util
open Names
open Nameops
-open Term
open Termops
+open Constr
open Namegen
open Environ
open Evd
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 209104ac32..38ed63c23d 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -10,7 +10,7 @@
open Util
open Names
-open Term
+open Constr
open Termops
open Evd
open EConstr
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 4934afa837..218b2671ec 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -481,7 +481,7 @@ and mk_arggoals sigma goal goalacc funty allargs =
let env = Goal.V82.env sigma goal in
raise (RefinerError (env,sigma,CannotApply (t, harg)))
in
- Array.smartfoldmap foldmap (goalacc, funty, sigma) allargs
+ Array.Smart.fold_left_map foldmap (goalacc, funty, sigma) allargs
and mk_casegoals sigma goal goalacc p c =
let env = Goal.V82.env sigma goal in
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 805635dfa4..7b79732249 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -24,7 +24,7 @@ open Decl_kinds
proof of mutually dependent theorems) *)
val start_proof :
- Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
+ Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
?init_tac:unit Proofview.tactic ->
Proof_global.proof_terminator -> unit
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 842003bc86..3abdd129e4 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -78,9 +78,11 @@ type proof_object = {
universes: UState.t;
}
+type opacity_flag = Opaque | Transparent
+
type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
- | Proved of Vernacexpr.opacity_flag *
+ | Proved of opacity_flag *
Misctypes.lident option *
proof_object
@@ -95,7 +97,7 @@ type pstate = {
proof : Proof.t;
strength : Decl_kinds.goal_kind;
mode : proof_mode CEphemeron.key;
- universe_decl: Univdecls.universe_decl;
+ universe_decl: UState.universe_decl;
}
type t = pstate list
@@ -236,13 +238,6 @@ let activate_proof_mode mode =
let disactivate_current_proof_mode () =
CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ())
-let default_universe_decl =
- let open Misctypes in
- { univdecl_instance = [];
- univdecl_extensible_instance = true;
- univdecl_constraints = Univ.Constraint.empty;
- univdecl_extensible_constraints = true }
-
(** [start_proof sigma id pl str goals terminator] starts a proof of name
[id] with goals [goals] (a list of pairs of environment and
conclusion); [str] describes what kind of theorem/definition this
@@ -251,7 +246,7 @@ let default_universe_decl =
end of the proof to close the proof. The proof is started in the
evar map [sigma] (which can typically contain universe
constraints), and with universe bindings pl. *)
-let start_proof sigma id ?(pl=default_universe_decl) str goals terminator =
+let start_proof sigma id ?(pl=UState.default_univ_decl) str goals terminator =
let initial_state = {
pid = id;
terminator = CEphemeron.create terminator;
@@ -263,7 +258,7 @@ let start_proof sigma id ?(pl=default_universe_decl) str goals terminator =
universe_decl = pl } in
push initial_state pstates
-let start_dependent_proof id ?(pl=default_universe_decl) str goals terminator =
+let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator =
let initial_state = {
pid = id;
terminator = CEphemeron.create terminator;
@@ -342,7 +337,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
normalise them for the kernel. *)
let subst_evar k =
Proof.in_proof proof (fun m -> Evd.existential_opt_value0 m k) in
- let nf = Universes.nf_evars_and_universes_opt_subst subst_evar
+ let nf = UnivSubst.nf_evars_and_universes_opt_subst subst_evar
(UState.subst universes) in
let make_body =
if poly || now then
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index bf35fd6599..0141cacb9e 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -48,10 +48,12 @@ type proof_object = {
universes: UState.t;
}
+type opacity_flag = Opaque | Transparent
+
type proof_ending =
| Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry *
UState.t
- | Proved of Vernacexpr.opacity_flag *
+ | Proved of opacity_flag *
Misctypes.lident option *
proof_object
type proof_terminator
@@ -69,14 +71,14 @@ val apply_terminator : proof_terminator -> proof_ending -> unit
evar map [sigma] (which can typically contain universe
constraints), and with universe bindings pl. *)
val start_proof :
- Evd.evar_map -> Names.Id.t -> ?pl:Univdecls.universe_decl ->
+ Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl ->
Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list ->
proof_terminator -> unit
(** Like [start_proof] except that there may be dependencies between
initial goals. *)
val start_dependent_proof :
- Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind ->
+ Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind ->
Proofview.telescope -> proof_terminator -> unit
(** Update the proofs global environment after a side-effecting command
@@ -128,7 +130,7 @@ val set_used_variables :
val get_used_variables : unit -> Context.Named.t option
(** Get the universe declaration associated to the current proof. *)
-val get_universe_decl : unit -> Univdecls.universe_decl
+val get_universe_decl : unit -> UState.universe_decl
module V82 : sig
val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 6fb4119387..03ebc32759 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -12,7 +12,7 @@ open Pp
open CErrors
open Util
open Names
-open Term
+open Constr
open EConstr
open Declarations
open Globnames
@@ -92,9 +92,9 @@ let cache_strategy (_,str) =
let subst_strategy (subs,(local,obj)) =
local,
- List.smartmap
+ List.Smart.map
(fun (k,ql as entry) ->
- let ql' = List.smartmap (Mod_subst.subst_evaluable_reference subs) ql in
+ let ql' = List.Smart.map (Mod_subst.subst_evaluable_reference subs) ql in
if ql==ql' then entry else (k,ql'))
obj
@@ -263,7 +263,7 @@ let subst_mps subst c =
EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
let subst_red_expr subs =
- Miscops.map_red_expr_gen
+ Redops.map_red_expr_gen
(subst_mps subs)
(Mod_subst.subst_evaluable_reference subs)
(Patternops.subst_pattern subs)
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 5a2d82977e..b64e7a2e5e 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -30,26 +30,19 @@ let typecheck_evar ev env sigma =
(** Typecheck the hypotheses. *)
let type_hyp (sigma, env) decl =
let t = NamedDecl.get_type decl in
- let evdref = ref sigma in
- let _ = Typing.e_sort_of env evdref t in
- let () = match decl with
- | LocalAssum _ -> ()
- | LocalDef (_,body,_) -> Typing.e_check env evdref body t
+ let sigma, _ = Typing.sort_of env sigma t in
+ let sigma = match decl with
+ | LocalAssum _ -> sigma
+ | LocalDef (_,body,_) -> Typing.check env sigma body t
in
- (!evdref, EConstr.push_named decl env)
+ (sigma, EConstr.push_named decl env)
in
let (common, changed) = extract_prefix env info in
let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in
let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
(** Typecheck the conclusion *)
- let evdref = ref sigma in
- let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
- !evdref
-
-let typecheck_proof c concl env sigma =
- let evdref = ref sigma in
- let () = Typing.e_check env evdref c concl in
- !evdref
+ let sigma, _ = Typing.sort_of env sigma (Evd.evar_concl info) in
+ sigma
let (pr_constrv,pr_constr) =
Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
@@ -93,7 +86,7 @@ let generic_refine ~typecheck f gl =
let fold accu ev = typecheck_evar ev env accu in
let sigma = if typecheck then Evd.fold_future_goals fold sigma evs else sigma in
(** Check that the refined term is typesafe *)
- let sigma = if typecheck then typecheck_proof c concl env sigma else sigma in
+ let sigma = if typecheck then Typing.check env sigma c concl else sigma in
(** Check that the goal itself does not appear in the refined term *)
let self = Proofview.Goal.goal gl in
let _ =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 5cd703a25c..0f83e16ec8 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -23,9 +23,12 @@ val pf_env : goal sigma -> Environ.env
val pf_hyps : goal sigma -> named_context
val unpackage : 'a sigma -> evar_map ref * 'a
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
val repackage : evar_map ref -> 'a -> 'a sigma
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
val apply_sig_tac :
evar_map ref -> (goal sigma -> goal list sigma) -> goal -> goal list
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
val refiner : rule -> tactic
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 1889054f86..092bb5c276 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -33,9 +33,11 @@ let re_sig it gc = { it = it; sigma = gc; }
type 'a sigma = 'a Evd.sigma;;
type tactic = Proof_type.tactic;;
+[@@@ocaml.warning "-3"]
let unpackage = Refiner.unpackage
let repackage = Refiner.repackage
let apply_sig_tac = Refiner.apply_sig_tac
+[@@@ocaml.warning "+3"]
let sig_it = Refiner.sig_it
let project = Refiner.project
@@ -73,7 +75,7 @@ let pf_ids_set_of_hyps gls =
let pf_get_new_id id gls =
next_ident_away id (pf_ids_set_of_hyps gls)
-let pf_global gls id = EConstr.of_constr (Universes.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
+let pf_global gls id = EConstr.of_constr (UnivGen.constr_of_global (Constrintern.construct_reference (pf_hyps gls) id))
let pf_reduction_of_red_expr gls re c =
let (redfun, _) = reduction_of_red_expr (pf_env gls) re in
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index de96f85104..31496fb3d5 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -30,9 +30,12 @@ val project : goal sigma -> evar_map
val re_sig : 'a -> evar_map -> 'a sigma
val unpackage : 'a sigma -> evar_map ref * 'a
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
val repackage : evar_map ref -> 'a -> 'a sigma
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
val apply_sig_tac :
evar_map ref -> (goal sigma -> (goal list) sigma) -> goal -> (goal list)
+[@@ocaml.deprecated "Do not use [evar_map ref]"]
val pf_concl : goal sigma -> types
val pf_env : goal sigma -> env
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 06:14:03 +0000