aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh6
-rw-r--r--plugins/ssr/ssrequality.ml32
-rw-r--r--tactics/declare.ml17
-rw-r--r--tactics/equality.ml49
-rw-r--r--tactics/equality.mli2
-rw-r--r--test-suite/success/RewriteRegisteredElim.v35
-rw-r--r--vernac/comAssumption.ml61
-rw-r--r--vernac/comAssumption.mli6
-rw-r--r--vernac/comFixpoint.ml13
-rw-r--r--vernac/comInductive.ml4
-rw-r--r--vernac/comProgramFixpoint.ml16
-rw-r--r--vernac/lemmas.ml3
-rw-r--r--vernac/vernacentries.ml8
13 files changed, 149 insertions, 103 deletions
diff --git a/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh b/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh
new file mode 100644
index 0000000000..413805e8e9
--- /dev/null
+++ b/dev/ci/user-overlays/10642-SkySkimmer-feedback-added-axiom.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "10642" ] || [ "$CI_BRANCH" = "feedback-added-axiom" ]; then
+
+ elpi_CI_REF=feedback-added-axiom
+ elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index aa1316f15e..4c6b7cdcb6 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -128,10 +128,9 @@ let newssrcongrtac arg ist gl =
x, re_sig si sigma in
let arr, gl = pf_mkSsrConst "ssr_congr_arrow" gl in
let ssr_congr lr = EConstr.mkApp (arr, lr) in
+ let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
(* here the two cases: simple equality or arrow *)
- let equality, _, eq_args, gl' =
- let eq, gl = pf_fresh_global Coqlib.(lib_ref "core.eq.type") gl in
- pf_saturate gl (EConstr.of_constr eq) 3 in
+ let equality, _, eq_args, gl' = pf_saturate gl (EConstr.of_constr eq) 3 in
tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args))
(fun ty -> congrtac (arg, Detyping.detype Detyping.Now false Id.Set.empty (pf_env gl) (project gl) ty) ist)
(fun () ->
@@ -336,17 +335,21 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
let sigma, p = (* The resulting goal *)
Evarutil.new_evar env sigma (beta (EConstr.Vars.subst1 new_rdx pred)) in
let pred = EConstr.mkNamedLambda (make_annot pattern_id Sorts.Relevant) rdx_ty pred in
- let elim, gl =
- let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
+ let sigma, elim =
let sort = elimination_sort_of_goal gl in
- let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in
- if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
- let elim, _ = destConst elim in
- let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
- let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in
- let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in
- mkConst c1', gl in
- let elim = EConstr.of_constr elim in
+ match Equality.eq_elimination_ref (dir = L2R) sort with
+ | Some r -> Evd.fresh_global env sigma r
+ | None ->
+ let ((kn, i) as ind, _), unfolded_c_ty = Tacred.reduce_to_quantified_ind env sigma c_ty in
+ let sort = elimination_sort_of_goal gl in
+ let sigma, elim = Evd.fresh_global env sigma (Indrec.lookup_eliminator env ind sort) in
+ if dir = R2L then sigma, elim else
+ let elim, _ = EConstr.destConst sigma elim in
+ let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
+ let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in
+ let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make2 mp l')) in
+ sigma, EConstr.of_constr (mkConst c1')
+ in
let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in
(* We check the proof is well typed *)
let sigma, proof_ty =
@@ -491,7 +494,8 @@ let rwprocess_rule dir rule gl =
| _ ->
let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in
EConstr.mkApp (pi2, ra), sigma in
- if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.True.type"))) then
+ let sigma,trty = Evd.fresh_global env sigma Coqlib.(lib_ref "core.True.type") in
+ if EConstr.eq_constr sigma a.(0) trty then
let s, sigma = sr sigma 2 in
loop (converse_dir d) sigma s a.(1) rs 0
else
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 61f9c3b1c5..e093a27728 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -243,11 +243,16 @@ let get_roles export eff =
in
List.map map export
+let feedback_axiom () = Feedback.(feedback AddedAxiom)
+let is_unsafe_typing_flags () =
+ let flags = Environ.typing_flags (Global.env()) in
+ not (flags.check_universes && flags.check_guarded)
+
let define_constant ~side_effect ~name cd =
let open Proof_global in
(* Logically define the constant and its subproofs, no libobject tampering *)
let in_section = Lib.sections_are_opened () in
- let export, decl = match cd with
+ let export, decl, unsafe = match cd with
| DefinitionEntry de ->
(* We deal with side effects *)
if not de.proof_entry_opaque then
@@ -257,19 +262,20 @@ let define_constant ~side_effect ~name cd =
let export = get_roles export eff in
let de = { de with proof_entry_body = Future.from_val (body, ()) } in
let cd = Entries.DefinitionEntry (cast_proof_entry de) in
- export, ConstantEntry (PureEntry, cd)
+ export, ConstantEntry (PureEntry, cd), false
else
let map (body, eff) = body, eff.Evd.seff_private in
let body = Future.chain de.proof_entry_body map in
let de = { de with proof_entry_body = body } in
let de = cast_opaque_proof_entry de in
- [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de)
+ [], ConstantEntry (EffectEntry, Entries.OpaqueEntry de), false
| ParameterEntry e ->
- [], ConstantEntry (PureEntry, Entries.ParameterEntry e)
+ [], ConstantEntry (PureEntry, Entries.ParameterEntry e), not (Lib.is_modtype_strict())
| PrimitiveEntry e ->
- [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e)
+ [], ConstantEntry (PureEntry, Entries.PrimitiveEntry e), false
in
let kn, eff = Global.add_constant ~side_effect ~in_section name decl in
+ if unsafe || is_unsafe_typing_flags() then feedback_axiom();
kn, eff, export
let declare_constant ?(local = ImportDefaultBehavior) ~name ~kind cd =
@@ -489,6 +495,7 @@ let declare_mind mie =
| ind::_ -> ind.mind_entry_typename
| [] -> CErrors.anomaly (Pp.str "cannot declare an empty list of inductives.") in
let (sp,kn as oname) = add_leaf id (inInductive mie) in
+ if is_unsafe_typing_flags() then feedback_axiom();
let mind = Global.mind_of_delta_kn kn in
let isprim = declare_projections mie.mind_entry_universes mind in
Impargs.declare_mib_implicits mind;
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 7c90c59f61..b9d718dd61 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -334,6 +334,21 @@ let jmeq_same_dom env sigma = function
| _, [dom1; _; dom2;_] -> is_conv env sigma dom1 dom2
| _ -> false
+let eq_elimination_ref l2r sort =
+ let name =
+ if l2r then
+ match sort with
+ | InProp -> "core.eq.ind_r"
+ | InSProp -> "core.eq.sind_r"
+ | InSet | InType -> "core.eq.rect_r"
+ else
+ match sort with
+ | InProp -> "core.eq.ind"
+ | InSProp -> "core.eq.sind"
+ | InSet | InType -> "core.eq.rect"
+ in
+ if Coqlib.has_ref name then Some (Coqlib.lib_ref name) else None
+
(* find_elim determines which elimination principle is necessary to
eliminate lbeq on sort_of_gl. *)
@@ -345,35 +360,35 @@ let find_elim hdcncl lft2rgt dep cls ot =
in
let inccl = Option.is_empty cls in
let env = Proofview.Goal.env gl in
- (* if (is_global Coqlib.glob_eq hdcncl || *)
- (* (is_global Coqlib.glob_jmeq hdcncl && *)
- (* jmeq_same_dom env sigma ot)) && not dep *)
- if (is_global_exists "core.eq.type" hdcncl ||
- (is_global_exists "core.JMeq.type" hdcncl
- && jmeq_same_dom env sigma ot)) && not dep
+ let is_eq = is_global_exists "core.eq.type" hdcncl in
+ let is_jmeq = is_global_exists "core.JMeq.type" hdcncl && jmeq_same_dom env sigma ot in
+ if (is_eq || is_jmeq) && not dep
then
+ let sort = elimination_sort_of_clause cls gl in
let c =
match EConstr.kind sigma hdcncl with
| Ind (ind_sp,u) ->
- let pr1 =
- lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl)
- in
begin match lft2rgt, cls with
| Some true, None
| Some false, Some _ ->
- let c1 = destConstRef pr1 in
- let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in
- let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in
- let c1' = Global.constant_of_delta_kn (KerName.make mp l') in
- begin
+ begin match if is_eq then eq_elimination_ref true sort else None with
+ | Some r -> destConstRef r
+ | None ->
+ let c1 = destConstRef (lookup_eliminator env ind_sp sort) in
+ let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in
+ let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in
+ let c1' = Global.constant_of_delta_kn (KerName.make mp l') in
try
- let _ = Global.lookup_constant c1' in
- c1'
+ let _ = Global.lookup_constant c1' in c1'
with Not_found ->
user_err ~hdr:"Equality.find_elim"
(str "Cannot find rewrite principle " ++ Label.print l' ++ str ".")
end
- | _ -> destConstRef pr1
+ | _ ->
+ begin match if is_eq then eq_elimination_ref false sort else None with
+ | Some r -> destConstRef r
+ | None -> destConstRef (lookup_eliminator env ind_sp sort)
+ end
end
| _ ->
(* cannot occur since we checked that we are in presence of
diff --git a/tactics/equality.mli b/tactics/equality.mli
index f8166bba2d..8225195ca7 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -29,6 +29,8 @@ type conditions =
| FirstSolved (* Use the first match whose side-conditions are solved *)
| AllMatches (* Rewrite all matches whose side-conditions are solved *)
+val eq_elimination_ref : orientation -> Sorts.family -> GlobRef.t option
+
val general_rewrite_bindings :
orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
?tac:(unit Proofview.tactic * conditions) -> constr with_bindings -> evars_flag -> unit Proofview.tactic
diff --git a/test-suite/success/RewriteRegisteredElim.v b/test-suite/success/RewriteRegisteredElim.v
new file mode 100644
index 0000000000..39b103747c
--- /dev/null
+++ b/test-suite/success/RewriteRegisteredElim.v
@@ -0,0 +1,35 @@
+
+Set Universe Polymorphism.
+
+Cumulative Inductive EQ {A} (x : A) : A -> Type
+ := EQ_refl : EQ x x.
+
+Register EQ as core.eq.type.
+
+Lemma renamed_EQ_rect {A} (x:A) (P : A -> Type)
+ (c : P x) (y : A) (e : EQ x y) : P y.
+Proof. destruct e. assumption. Qed.
+
+Register renamed_EQ_rect as core.eq.rect.
+Register renamed_EQ_rect as core.eq.ind.
+
+Lemma renamed_EQ_rect_r {A} (x:A) (P : A -> Type)
+ (c : P x) (y : A) (e : EQ y x) : P y.
+Proof. destruct e. assumption. Qed.
+
+Register renamed_EQ_rect_r as core.eq.rect_r.
+Register renamed_EQ_rect_r as core.eq.ind_r.
+
+Lemma EQ_sym1 {A} {x y : A} (e : EQ x y) : EQ y x.
+Proof. rewrite e. reflexivity. Qed.
+
+Lemma EQ_sym2 {A} {x y : A} (e : EQ x y) : EQ y x.
+Proof. rewrite <- e. reflexivity. Qed.
+
+Require Import ssreflect.
+
+Lemma ssr_EQ_sym1 {A} {x y : A} (e : EQ x y) : EQ y x.
+Proof. rewrite e. reflexivity. Qed.
+
+Lemma ssr_EQ_sym2 {A} {x y : A} (e : EQ x y) : EQ y x.
+Proof. rewrite -e. reflexivity. Qed.
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index d59d471d5f..7d365db85c 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -59,7 +59,7 @@ match scope with
let sigma = Evd.from_env env in
let () = Classes.declare_instance env sigma None true r in
let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in
- (r,Univ.Instance.empty,true)
+ (r,Univ.Instance.empty)
| Global local ->
let do_instance = should_axiom_into_instance kind in
@@ -84,7 +84,7 @@ match scope with
| Polymorphic_entry (_, univs) -> Univ.UContext.instance univs
| Monomorphic_entry _ -> Univ.Instance.empty
in
- (gr,inst,Lib.is_modtype_strict ())
+ (gr,inst)
let interp_assumption ~program_mode sigma env impls c =
let sigma, (ty, impls) = interp_type_evars_impls ~program_mode env sigma ~impls c in
@@ -98,14 +98,13 @@ let next_uctx =
| Monomorphic_entry _ -> empty_uctx
let declare_assumptions idl is_coe ~scope ~poly ~kind typ uctx pl imps nl =
- let refs, status, _ =
- List.fold_left (fun (refs,status,uctx) id ->
- let ref',u',status' =
- declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps false nl id in
- (ref',u')::refs, status' && status, next_uctx uctx)
- ([],true,uctx) idl
+ let refs, _ =
+ List.fold_left (fun (refs,uctx) id ->
+ let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps false nl id in
+ ref::refs, next_uctx uctx)
+ ([],uctx) idl
in
- List.rev refs, status
+ List.rev refs
let maybe_error_many_udecls = function
@@ -178,15 +177,17 @@ let do_assumptions ~program_mode ~poly ~scope ~kind nl l =
let sigma = Evd.restrict_universe_context sigma uvars in
let uctx = Evd.check_univ_decl ~poly sigma udecl in
let ubinders = Evd.universe_binders sigma in
- pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),typ,imps) ->
+ let _, _ = List.fold_left (fun (subst,uctx) ((is_coe,idl),typ,imps) ->
let typ = replace_vars subst typ in
- let refs, status' = declare_assumptions idl is_coe ~poly ~scope ~kind typ uctx ubinders imps nl in
+ let refs = declare_assumptions idl is_coe ~poly ~scope ~kind typ uctx ubinders imps nl in
let subst' = List.map2
(fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
idl refs
in
- subst'@subst, status' && status, next_uctx uctx)
- ([], true, uctx) l)
+ subst'@subst, next_uctx uctx)
+ ([], uctx) l
+ in
+ ()
let do_primitive id prim typopt =
if Lib.sections_are_opened () then
@@ -270,41 +271,43 @@ let context ~poly l =
Monomorphic_entry Univ.ContextSet.empty
end
in
- let fn status (name, b, t) =
+ let fn (name, b, t) =
let b, t = Option.map (EConstr.to_constr sigma) b, EConstr.to_constr sigma t in
if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
(* Declare the universe context once *)
let kind = Decls.(IsAssumption Logical) in
let decl = match b with
- | None ->
- Declare.ParameterEntry (None,(t,univs),None)
- | Some b ->
- let entry = Declare.definition_entry ~univs ~types:t b in
- Declare.DefinitionEntry entry
+ | None ->
+ Declare.ParameterEntry (None,(t,univs),None)
+ | Some b ->
+ let entry = Declare.definition_entry ~univs ~types:t b in
+ Declare.DefinitionEntry entry
in
let cst = Declare.declare_constant ~name ~kind decl in
let env = Global.env () in
Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (GlobRef.ConstRef cst);
- status
+ ()
else
let test x = match x.CAst.v with
- | Some (Name id',_) -> Id.equal name id'
- | _ -> false
+ | Some (Name id',_) -> Id.equal name id'
+ | _ -> false
in
let impl = List.exists test impls in
let scope =
if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in
- let nstatus = match b with
+ match b with
| None ->
- pi3 (declare_assumption false ~scope ~poly ~kind:Decls.Context t univs UnivNames.empty_binders [] impl
- Declaremods.NoInline (CAst.make name))
+ let _, _ =
+ declare_assumption false ~scope ~poly ~kind:Decls.Context t
+ univs UnivNames.empty_binders [] impl
+ Declaremods.NoInline (CAst.make name)
+ in
+ ()
| Some b ->
let entry = Declare.definition_entry ~univs ~types:t b in
let _gr = DeclareDef.declare_definition
~name ~scope:DeclareDef.Discharge
~kind:Decls.Definition UnivNames.empty_binders entry [] in
- Lib.sections_are_opened () || Lib.is_modtype_strict ()
- in
- status && nstatus
+ ()
in
- List.fold_left fn true (List.rev ctx)
+ List.iter fn (List.rev ctx)
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 028ed39656..1632c3d578 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -21,7 +21,7 @@ val do_assumptions
-> kind:Decls.assumption_object_kind
-> Declaremods.inline
-> (ident_decl list * constr_expr) with_coercion list
- -> bool
+ -> unit
(** returns [false] if the assumption is neither local to a section,
nor in a module type and meant to be instantiated. *)
@@ -37,7 +37,7 @@ val declare_assumption
-> bool (** implicit *)
-> Declaremods.inline
-> variable CAst.t
- -> GlobRef.t * Univ.Instance.t * bool
+ -> GlobRef.t * Univ.Instance.t
(** Context command *)
@@ -46,6 +46,6 @@ val declare_assumption
val context
: poly:bool
-> local_binder_expr list
- -> bool
+ -> unit
val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 74c9bc2886..b6843eab33 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -323,11 +323,6 @@ let adjust_rec_order ~structonly binders rec_order =
in
Option.map (extract_decreasing_argument ~structonly) rec_order
-let check_safe () =
- let open Declarations in
- let flags = Environ.typing_flags (Global.env ()) in
- flags.check_universes && flags.check_guarded
-
let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) =
let fixl = List.map (fun fix ->
Vernacexpr.{ fix
@@ -339,13 +334,11 @@ let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) =
let do_fixpoint_interactive ~scope ~poly l : Lemmas.t =
let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in
- if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
lemma
let do_fixpoint ~scope ~poly l =
let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
- declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns;
- if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+ declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns
let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in
@@ -355,10 +348,8 @@ let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) =
let do_cofixpoint_interactive ~scope ~poly l =
let cofix, ntns = do_cofixpoint_common l in
let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in
- if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
lemma
let do_cofixpoint ~scope ~poly l =
let cofix, ntns = do_cofixpoint_common l in
- declare_fixpoint_generic ~scope ~poly cofix ntns;
- if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+ declare_fixpoint_generic ~scope ~poly cofix ntns
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 664010c917..adbe196699 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -567,9 +567,7 @@ let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uni
(* Declare the possible notations of inductive types *)
List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
(* Declare the coercions *)
- List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes;
- (* If positivity is assumed declares itself as unsafe. *)
- if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else ()
+ List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes
(** Prepare a "match" template for a given inductive type.
For each branch of the match, we list the constructor name
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index c6e68effd7..3497e6369f 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -292,7 +292,7 @@ let do_program_recursive ~scope ~poly fixkind fixl =
let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in
Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind
-let do_program_fixpoint ~scope ~poly l =
+let do_fixpoint ~scope ~poly l =
let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in
match g, l with
| [Some { CAst.v = CWfRec (n,r) }],
@@ -322,19 +322,9 @@ let do_program_fixpoint ~scope ~poly l =
do_program_recursive ~scope ~poly fixkind l
| _, _ ->
- user_err ~hdr:"do_program_fixpoint"
+ user_err ~hdr:"do_fixpoint"
(str "Well-founded fixpoints not allowed in mutually recursive blocks")
-let check_safe () =
- let open Declarations in
- let flags = Environ.typing_flags (Global.env ()) in
- flags.check_universes && flags.check_guarded
-
-let do_fixpoint ~scope ~poly l =
- do_program_fixpoint ~scope ~poly l;
- if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
-
let do_cofixpoint ~scope ~poly fixl =
let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in
- do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl;
- if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
+ do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 6a754a0cde..adfb058942 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -336,8 +336,7 @@ let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs othe
let () = Declare.assumption_message name in
Declare.declare_univ_binders (GlobRef.ConstRef kn) (UState.universe_binders ctx);
(* This takes care of the implicits and hook for the current constant*)
- process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms;
- Feedback.feedback Feedback.AddedAxiom
+ process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (GlobRef.ConstRef kn) impargs other_thms
let save_lemma_admitted ~(lemma : t) : unit =
(* Used for printing in recthms *)
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9af8d8b67c..bc51dd46f3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -604,8 +604,7 @@ let vernac_assumption ~atts discharge kind l nl =
match scope with
| DeclareDef.Global _ -> Dumpglob.dump_definition lid false "ax"
| DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
- let status = ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l in
- if not status then Feedback.feedback Feedback.AddedAxiom
+ ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
let is_polymorphic_inductive_cumulativity =
declare_bool_option_and_ref ~depr:false ~value:false
@@ -1074,9 +1073,6 @@ let vernac_declare_instance ~atts id bl inst pri =
let global = not (make_section_locality locality) in
Classes.declare_new_instance ~program_mode:program ~global ~poly id bl inst pri
-let vernac_context ~poly l =
- if not (ComAssumption.context ~poly l) then Feedback.feedback Feedback.AddedAxiom
-
let vernac_existing_instance ~section_local insts =
let glob = not section_local in
List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts
@@ -2439,7 +2435,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
| VernacDeclareInstance (id, bl, inst, info) ->
VtDefault(fun () -> vernac_declare_instance ~atts id bl inst info)
| VernacContext sup ->
- VtDefault(fun () -> vernac_context ~poly:(only_polymorphism atts) sup)
+ VtDefault(fun () -> ComAssumption.context ~poly:(only_polymorphism atts) sup)
| VernacExistingInstance insts ->
VtDefault(fun () -> with_section_locality ~atts vernac_existing_instance insts)
| VernacExistingClass id ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 04:08:58 +0000