aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/funind/gen_principle.ml107
-rw-r--r--vernac/auto_ind_decl.ml6
-rw-r--r--vernac/declare.ml4
-rw-r--r--vernac/declare.mli2
-rw-r--r--vernac/obligations.ml2
-rw-r--r--vernac/pfedit.ml12
-rw-r--r--vernac/proof_global.ml7
-rw-r--r--vernac/vernacentries.ml2
8 files changed, 66 insertions, 76 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 55e659d487..07f578d2a8 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -191,61 +191,35 @@ let prepare_body {Vernacexpr.binders} rt =
let fun_args, rt' = chop_rlambda_n n rt in
(fun_args, rt')
-let build_functional_principle ?(opaque = Declare.Transparent)
- (evd : Evd.evar_map ref) old_princ_type sorts funs _i proof_tac hook =
+let build_functional_principle (sigma : Evd.evar_map) old_princ_type sorts funs
+ _i proof_tac hook =
(* First we get the type of the old graph principle *)
let mutr_nparams =
- (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type))
+ (Tactics.compute_elim_sig sigma (EConstr.of_constr old_princ_type))
.Tactics.nparams
in
- (* let time1 = System.get_time () in *)
let new_principle_type =
Functional_principles_types.compute_new_princ_type_from_rel
(Array.map Constr.mkConstU funs)
sorts old_princ_type
in
- (* let time2 = System.get_time () in *)
- (* Pp.msgnl (str "computing principle type := " ++ System.fmt_time_difference time1 time2); *)
- let new_princ_name =
- Namegen.next_ident_away_in_goal
- (Id.of_string "___________princ_________")
- Id.Set.empty
- in
let sigma, _ =
- Typing.type_of ~refresh:true (Global.env ()) !evd
- (EConstr.of_constr new_principle_type)
- in
- evd := sigma;
- let hook = DeclareDef.Hook.make (hook new_principle_type) in
- let lemma =
- Lemmas.start_lemma ~name:new_princ_name ~poly:false !evd
+ Typing.type_of ~refresh:true (Global.env ()) sigma
(EConstr.of_constr new_principle_type)
in
- (* let _tim1 = System.get_time () in *)
let map (c, u) = EConstr.mkConstU (c, EConstr.EInstance.make u) in
- let lemma, _ =
- Lemmas.by
- (Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams))
- lemma
+ let ftac =
+ Proofview.V82.tactic (proof_tac (Array.map map funs) mutr_nparams)
in
- (* let _tim2 = System.get_time () in *)
- (* begin *)
- (* let dur1 = System.time_difference tim1 tim2 in *)
- (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
- (* end; *)
- let {Declare.entries} =
- Lemmas.pf_fold
- (Declare.close_proof ~opaque ~keep_body_ucst_separate:false)
- lemma
+ let env = Global.env () in
+ let uctx = Evd.evar_universe_context sigma in
+ let typ = EConstr.of_constr new_principle_type in
+ let body, typ, univs, _safe, _uctx =
+ Declare.build_by_tactic env ~uctx ~poly:false ~typ ftac
in
- match entries with
- | [entry] -> (entry, hook)
- | _ ->
- CErrors.anomaly
- Pp.(
- str
- "[build_functional_principle] close_proof returned more than one \
- proof term")
+ (* uctx was ignored before *)
+ let hook = DeclareDef.Hook.make (hook new_principle_type) in
+ (body, typ, univs, hook, sigma)
let change_property_sort evd toSort princ princName =
let open Context.Rel.Declaration in
@@ -333,14 +307,16 @@ let generate_functional_principle (evd : Evd.evar_map ref) old_princ_type sorts
register_with_sort Sorts.InProp;
register_with_sort Sorts.InSet )
in
- let entry, hook =
- build_functional_principle evd old_princ_type new_sorts funs i proof_tac
+ let body, types, univs, hook, sigma0 =
+ build_functional_principle !evd old_princ_type new_sorts funs i proof_tac
hook
in
+ evd := sigma0;
(* Pr 1278 :
Don't forget to close the goal if an error is raised !!!!
*)
let uctx = Evd.evar_universe_context sigma in
+ let entry = Declare.definition_entry ~univs ?types body in
let (_ : Names.GlobRef.t) =
DeclareDef.declare_entry ~name:new_princ_name ~hook
~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
@@ -1334,8 +1310,7 @@ let get_funs_constant mp =
in
l_const
-let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) :
- Evd.side_effects Declare.proof_entry list =
+let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : _ list =
let exception Found_type of int in
let env = Global.env () in
let funs = List.map fst fas in
@@ -1402,18 +1377,19 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) :
if Declareops.is_opaque (Global.lookup_constant equation) then Opaque
else Transparent
in
- let entry, _hook =
+ let body, typ, univs, _hook, sigma0 =
try
- build_functional_principle ~opaque evd first_type (Array.of_list sorts)
+ build_functional_principle !evd first_type (Array.of_list sorts)
this_block_funs 0
(Functional_principles_proofs.prove_princ_for_struct evd false 0
(Array.of_list (List.map fst funs)))
(fun _ _ -> ())
with e when CErrors.noncritical e -> raise (Defining_principle e)
in
+ evd := sigma0;
incr i;
(* The others are just deduced *)
- if List.is_empty other_princ_types then [entry]
+ if List.is_empty other_princ_types then [(body, typ, univs, opaque)]
else
let other_fun_princ_types =
let funs = Array.map Constr.mkConstU this_block_funs in
@@ -1422,10 +1398,8 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) :
(Functional_principles_types.compute_new_princ_type_from_rel funs sorts)
other_princ_types
in
- let first_princ_body = entry.Declare.proof_entry_body in
- let ctxt, fix =
- Term.decompose_lam_assum (fst (fst (Future.force first_princ_body)))
- in
+ let first_princ_body = body in
+ let ctxt, fix = Term.decompose_lam_assum first_princ_body in
(* the principle has for forall ...., fix .*)
let (idxs, _), ((_, ta, _) as decl) = Constr.destFix fix in
let other_result =
@@ -1457,8 +1431,8 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) :
(* If we reach this point, the two principle are not mutually recursive
We fall back to the previous method
*)
- let entry, _hook =
- build_functional_principle evd
+ let body, typ, univs, _hook, sigma0 =
+ build_functional_principle !evd
(List.nth other_princ_types (!i - 1))
(Array.of_list sorts) this_block_funs !i
(Functional_principles_proofs.prove_princ_for_struct evd false
@@ -1466,15 +1440,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) :
(Array.of_list (List.map fst funs)))
(fun _ _ -> ())
in
- entry
+ evd := sigma0;
+ (body, typ, univs, opaque)
with Found_type i ->
let princ_body =
Termops.it_mkLambda_or_LetIn (Constr.mkFix ((idxs, i), decl)) ctxt
in
- Declare.definition_entry ~types:scheme_type princ_body)
+ (princ_body, Some scheme_type, univs, opaque))
other_fun_princ_types
in
- entry :: other_result
+ (body, typ, univs, opaque) :: other_result
(* [derive_correctness funs graphs] create correctness and completeness
lemmas for each function in [funs] w.r.t. [graphs]
@@ -1527,11 +1502,8 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
with Not_found ->
Array.of_list
(List.map
- (fun entry ->
- ( EConstr.of_constr
- (fst (fst (Future.force entry.Declare.proof_entry_body)))
- , EConstr.of_constr (Option.get entry.Declare.proof_entry_type)
- ))
+ (fun (body, typ, _opaque, _univs) ->
+ (EConstr.of_constr body, EConstr.of_constr (Option.get typ)))
(make_scheme evd
(Array.map_to_list (fun const -> (const, Sorts.InType)) funs)))
in
@@ -2225,11 +2197,14 @@ let build_scheme fas =
in
let bodies_types = make_scheme evd pconstants in
List.iter2
- (fun (princ_id, _, _) def_entry ->
- ignore
- (Declare.declare_constant ~name:princ_id
- ~kind:Decls.(IsProof Theorem)
- (Declare.DefinitionEntry def_entry));
+ (fun (princ_id, _, _) (body, types, univs, opaque) ->
+ let (_ : Constant.t) =
+ let opaque = if opaque = Declare.Opaque then true else false in
+ let def_entry = Declare.definition_entry ~univs ~opaque ?types body in
+ Declare.declare_constant ~name:princ_id
+ ~kind:Decls.(IsProof Theorem)
+ (Declare.DefinitionEntry def_entry)
+ in
Declare.definition_message princ_id)
fas bodies_types
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index ebea5e146c..743d1d2026 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -710,7 +710,7 @@ let make_bl_scheme mode mind =
let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
let side_eff = side_effect_of_mode mode in
let bl_goal = EConstr.of_constr bl_goal in
- let (ans, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal
+ let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:bl_goal
(compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, EConstr.EInstance.empty) lnamesparrec nparrec)
in
([|ans|], ctx)
@@ -843,7 +843,7 @@ let make_lb_scheme mode mind =
let uctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
let side_eff = side_effect_of_mode mode in
let lb_goal = EConstr.of_constr lb_goal in
- let (ans, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal
+ let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx ~typ:lb_goal
(compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
in
([|ans|], ctx)
@@ -1014,7 +1014,7 @@ let make_eq_decidability mode mind =
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
let side_eff = side_effect_of_mode mode in
- let (ans, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx
+ let (ans, _, _, _, ctx) = Declare.build_by_tactic ~poly:false ~side_eff (Global.env()) ~uctx
~typ:(EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec))
(compute_dec_tact ind lnamesparrec nparrec)
in
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 357f58feea..95e573a671 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -762,7 +762,7 @@ let build_constant_by_tactic ~name ?(opaque=Transparent) ~uctx ~sign ~poly typ t
let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
let sign = Environ.(val_of_named_context (named_context env)) in
- let ce, status, univs = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
+ let ce, status, uctx = build_constant_by_tactic ~name ~uctx ~sign ~poly typ tac in
let cb, uctx =
if side_eff then inline_private_constants ~uctx env ce
else
@@ -770,7 +770,7 @@ let build_by_tactic ?(side_eff=true) env ~uctx ~poly ~typ tac =
let (cb, ctx), _eff = Future.force ce.proof_entry_body in
cb, UState.merge ~sideff:false Evd.univ_rigid uctx ctx
in
- cb, ce.proof_entry_type, status, univs
+ cb, ce.proof_entry_type, ce.proof_entry_universes, status, uctx
let declare_abstract ~name ~poly ~kind ~sign ~secsign ~opaque ~solve_tac sigma concl =
(* EJGA: flush_and_check_evars is only used in abstract, could we
diff --git a/vernac/declare.mli b/vernac/declare.mli
index e23e148ddc..a297f25868 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -249,7 +249,7 @@ val build_by_tactic
-> poly:bool
-> typ:EConstr.types
-> unit Proofview.tactic
- -> Constr.constr * Constr.types option * bool * UState.t
+ -> Constr.constr * Constr.types option * Entries.universes_entry * bool * UState.t
(** {6 Helpers to obtain proof state when in an interactive proof } *)
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 060f069419..bed593234b 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -133,7 +133,7 @@ let solve_by_tac ?loc name evi t poly uctx =
try
(* the status is dropped. *)
let env = Global.env () in
- let body, types, _, uctx =
+ let body, types, _univs, _, uctx =
Declare.build_by_tactic env ~uctx ~poly ~typ:evi.evar_concl t in
Inductiveops.control_only_guard env (Evd.from_ctx uctx) (EConstr.of_constr body);
Some (body, types, uctx)
diff --git a/vernac/pfedit.ml b/vernac/pfedit.ml
index d6b9592176..e6c66ee503 100644
--- a/vernac/pfedit.ml
+++ b/vernac/pfedit.ml
@@ -1,9 +1,19 @@
(* Compat API / *)
let get_current_context = Declare.get_current_context
+[@@ocaml.deprecated "Use [Declare.get_current_context]"]
let solve = Proof.solve
+[@@ocaml.deprecated "Use [Proof.solve]"]
let by = Declare.by
+[@@ocaml.deprecated "Use [Declare.by]"]
let refine_by_tactic = Proof.refine_by_tactic
+[@@ocaml.deprecated "Use [Proof.refine_by_tactic]"]
(* We don't want to export this anymore, but we do for now *)
-let build_by_tactic = Declare.build_by_tactic
+let build_by_tactic ?side_eff env ~uctx ~poly ~typ tac =
+ let b, t, _unis, safe, uctx =
+ Declare.build_by_tactic ?side_eff env ~uctx ~poly ~typ tac in
+ b, t, safe, uctx
+[@@ocaml.deprecated "Use [Proof.build_by_tactic]"]
+
let build_constant_by_tactic = Declare.build_constant_by_tactic
+[@@ocaml.deprecated "Use [Proof.build_constant_by_tactic]"]
diff --git a/vernac/proof_global.ml b/vernac/proof_global.ml
index b6c07042e2..54d1db44a4 100644
--- a/vernac/proof_global.ml
+++ b/vernac/proof_global.ml
@@ -1,7 +1,12 @@
(* compatibility module; can be removed once we agree on the API *)
type t = Declare.Proof.t
+[@@ocaml.deprecated "Use [Declare.Proof.t]"]
let map_proof = Declare.Proof.map_proof
+[@@ocaml.deprecated "Use [Declare.Proof.map_proof]"]
let get_proof = Declare.Proof.get_proof
+[@@ocaml.deprecated "Use [Declare.Proof.get_proof]"]
-type opacity_flag = Declare.opacity_flag = Opaque | Transparent
+type opacity_flag = Declare.opacity_flag =
+ | Opaque [@ocaml.deprecated "Use [Declare.Opaque]"]
+ | Transparent [@ocaml.deprecated "Use [Declare.Transparent]"]
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index df39c617d3..df94f69cf6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -475,7 +475,7 @@ let program_inference_hook env sigma ev =
Evarutil.is_ground_term sigma concl)
then None
else
- let c, _, _, ctx =
+ let c, _, _, _, ctx =
Declare.build_by_tactic ~poly:false env ~uctx:(Evd.evar_universe_context sigma) ~typ:concl tac
in
Some (Evd.set_universe_context sigma ctx, EConstr.of_constr c)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:37:01 +0000