aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/funind/gen_principle.ml53
-rw-r--r--tactics/ind_tables.ml12
-rw-r--r--vernac/declareObl.ml14
-rw-r--r--vernac/indschemes.ml20
-rw-r--r--vernac/record.ml10
5 files changed, 33 insertions, 76 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 352b21a15a..92b7f2accf 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -164,7 +164,7 @@ let prepare_body { Vernacexpr.binders } rt =
let fun_args,rt' = chop_rlambda_n n rt in
(fun_args,rt')
-let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
+let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) interactive_proof 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.nparams in
(* let time1 = System.get_time () in *)
@@ -199,10 +199,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
(* end; *)
let open Proof_global in
- let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+ let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in
match entries with
| [entry] ->
- name, entry, hook
+ entry, hook
| _ ->
CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
@@ -282,7 +282,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
register_with_sort Sorts.InProp;
register_with_sort Sorts.InSet
in
- let id,entry,hook =
+ let entry, hook =
build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
proof_tac hook
in
@@ -1219,9 +1219,21 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
s::l_schemes -> s,l_schemes
| _ -> CErrors.anomaly (Pp.str "")
in
- let _,const,_ =
+ let opaque =
+ let finfos =
+ match find_Function_infos (fst first_fun) with
+ | None -> raise Not_found
+ | Some finfos -> finfos
+ in
+ let open Proof_global in
+ match finfos.equation_lemma with
+ | None -> Transparent (* non recursive definition *)
+ | Some equation ->
+ if Declareops.is_opaque (Global.lookup_constant equation) then Opaque else Transparent
+ in
+ let entry, _hook =
try
- build_functional_principle evd false
+ build_functional_principle ~opaque evd false
first_type
(Array.of_list sorts)
this_block_funs
@@ -1233,29 +1245,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
in
incr i;
- let opacity =
- let finfos =
- match find_Function_infos (fst first_fun) with
- | None -> raise Not_found
- | Some finfos -> finfos
- in
- match finfos.equation_lemma with
- | None -> false (* non recursive definition *)
- | Some equation ->
- Declareops.is_opaque (Global.lookup_constant equation)
- in
- let const = {const with Declare.proof_entry_opaque = opacity } in
(* The others are just deduced *)
if List.is_empty other_princ_types
- then
- [const]
+ then [entry]
else
let other_fun_princ_types =
let funs = Array.map Constr.mkConstU this_block_funs in
let sorts = Array.of_list sorts in
List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types
in
- let first_princ_body,first_princ_type = Declare.(const.proof_entry_body, const.proof_entry_type) in
+ let first_princ_body,first_princ_type = Declare.(entry.proof_entry_body, entry.proof_entry_type) in
let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in
let other_result =
@@ -1282,7 +1281,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
(* If we reach this point, the two principle are not mutually recursive
We fall back to the previous method
*)
- let _,const,_ =
+ let entry, _hook =
build_functional_principle
evd
false
@@ -1293,20 +1292,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
(Functional_principles_proofs.prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs)))
(fun _ _ -> ())
in
- const
+ entry
with Found_type i ->
let princ_body =
Termops.it_mkLambda_or_LetIn (Constr.mkFix((idxs,i),decl)) ctxt
in
- { const with
- Declare.proof_entry_body =
- (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects));
- proof_entry_type = Some scheme_type
- }
+ Declare.definition_entry ~types:scheme_type princ_body
)
other_fun_princ_types
in
- const::other_result
+ entry::other_result
(* [derive_correctness funs graphs] create correctness and completeness
lemmas for each function in [funs] w.r.t. [graphs]
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 1f973ace6f..54393dce00 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -124,17 +124,7 @@ let define internal role id c poly univs =
let ctx = UState.minimize univs in
let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
let univs = UState.univ_entry ~poly ctx in
- let entry = {
- Declare.proof_entry_body =
- Future.from_val ((c,Univ.ContextSet.empty),
- Evd.empty_side_effects);
- proof_entry_secctx = None;
- proof_entry_type = None;
- proof_entry_universes = univs;
- proof_entry_opaque = false;
- proof_entry_inline_code = false;
- proof_entry_feedback = None;
- } in
+ let entry = Declare.definition_entry ~univs c in
let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in
let () = match internal with
| InternalTacticRequest -> ()
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 9c8213ad8a..e3cffa8523 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -149,18 +149,8 @@ let declare_obligation prg obl body ty uctx =
if get_shrink_obligations () && not poly then shrink_body body ty
else ([], body, ty, [||])
in
- let body =
- ((body, Univ.ContextSet.empty), Evd.empty_side_effects)
- in
- let ce =
- { Declare.proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body
- ; proof_entry_secctx = None
- ; proof_entry_type = ty
- ; proof_entry_universes = uctx
- ; proof_entry_opaque = opaque
- ; proof_entry_inline_code = false
- ; proof_entry_feedback = None }
- in
+ let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in
+
(* ppedrot: seems legit to have obligations as local *)
let constant =
Declare.declare_constant ~name:obl.obl_name
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 18955c2ba3..a6c577a878 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -98,19 +98,11 @@ let () =
(* Util *)
-let define ~poly name sigma c t =
+let define ~poly name sigma c types =
let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in
let univs = Evd.univ_entry ~poly sigma in
- let kn = f ~name
- (DefinitionEntry
- { proof_entry_body = c;
- proof_entry_secctx = None;
- proof_entry_type = t;
- proof_entry_universes = univs;
- proof_entry_opaque = false;
- proof_entry_inline_code = false;
- proof_entry_feedback = None;
- }) in
+ let entry = Declare.definition_entry ~univs ?types c in
+ let kn = f ~name (DefinitionEntry entry) in
definition_message name;
kn
@@ -411,8 +403,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
let declare decl fi lrecref =
let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
let decltype = EConstr.to_constr sigma decltype in
- let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in
- let cst = define ~poly fi sigma proof_output (Some decltype) in
+ let cst = define ~poly fi sigma decl (Some decltype) in
GlobRef.ConstRef cst :: lrecref
in
let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -533,7 +524,6 @@ let do_combined_scheme name schemes =
schemes
in
let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
- let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Evd.empty_side_effects) in
(* It is possible for the constants to have different universe
polymorphism from each other, however that is only when the user
manually defined at least one of them (as Scheme would pick the
@@ -541,7 +531,7 @@ let do_combined_scheme name schemes =
some other polymorphism they can also manually define the
combined scheme. *)
let poly = Global.is_polymorphic (GlobRef.ConstRef (List.hd csts)) in
- ignore (define ~poly name.v sigma proof_output (Some typ));
+ ignore (define ~poly name.v sigma body (Some typ));
fixpoint_message None [name.v]
(**********************************************************************)
diff --git a/vernac/record.ml b/vernac/record.ml
index 1bb8ddf5dc..11237f3873 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -340,15 +340,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
let projtyp =
it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
try
- let entry = {
- proof_entry_body =
- Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects);
- proof_entry_secctx = None;
- proof_entry_type = Some projtyp;
- proof_entry_universes = ctx;
- proof_entry_opaque = false;
- proof_entry_inline_code = false;
- proof_entry_feedback = None } in
+ let entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in
let kind = Decls.IsDefinition kind in
let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in
let constr_fip =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:04:45 +0000