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.ml9
-rw-r--r--proofs/pfedit.ml3
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--proofs/proof_global.ml23
-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.mli5
12 files changed, 46 insertions, 48 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..95c30d8159 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -309,9 +309,10 @@ let check_meta_variables env sigma c =
let check_conv_leq_goal env sigma arg ty conclty =
if !check then
- let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
- if b then evm
- else raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
+ let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
+ match ans with
+ | Some evm -> evm
+ | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
else sigma
exception Stop of EConstr.t list
@@ -481,7 +482,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.ml b/proofs/pfedit.ml
index 03c0969faa..678c3ea3f7 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -200,8 +200,7 @@ let refine_by_tactic env sigma ty tac =
| [c, _] -> c
| _ -> assert false
in
- let ans = Reductionops.nf_evar sigma ans in
- let ans = EConstr.Unsafe.to_constr ans in
+ let ans = EConstr.to_constr ~abort_on_undefined_evars:false sigma ans in
(** [neff] contains the freshly generated side-effects *)
let neff = Evd.eval_side_effects sigma in
(** Reset the old side-effects *)
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..9463793566 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
@@ -442,8 +437,8 @@ let return_proof ?(allow_partial=false) () =
(** ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
side-effects... This may explain why one need to uniquize side-effects
thereafter... *)
- let proofs =
- List.map (fun (c, _) -> (Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr c), eff)) initial_goals in
+ let proofs =
+ List.map (fun (c, _) -> (EConstr.to_constr evd c, eff)) initial_goals in
proofs, Evd.evar_universe_context evd
let close_future_proof ~feedback_id proof =
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 770d0940a3..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
@@ -95,7 +98,7 @@ val pr_glls : goal list sigma -> Pp.t
(* Variants of [Tacmach] functions built with the new proof engine *)
module New : sig
val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a
- val pf_global : Id.t -> Proofview.Goal.t -> Globnames.global_reference
+ val pf_global : Id.t -> Proofview.Goal.t -> GlobRef.t
(** FIXME: encapsulate the level in an existential type. *)
val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 13:12:36 +0000