allwarn

File "./theories/Logic/ExtensionalityFacts.v", line 95, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
FunctExt_iff_EqDeltaProjs.u1 <= Delta.u0
FunctExt_iff_EqDeltaProjs.u1 <= diagonal_projs_same_behavior.u0
FunctExt_iff_EqDeltaProjs.u1 <= FunctExt_iff_EqDeltaProjs.u0
FunctExt_iff_EqDeltaProjs.u1 = FunctExt_iff_EqDeltaProjs.u2
[private-mono,fragile,default]
File "./theories/Logic/ExtensionalityFacts.v", line 104, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
FunctExt_UniqInverse.u2 <= FunctExt_UniqInverse.u1
FunctExt_UniqInverse.u3 <= FunctExt_UniqInverse.u0
[private-mono,fragile,default]
File "./theories/Logic/ExtensionalityFacts.v", line 110, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
UniqInverse_EqDeltaProjs.u2 <= delta.u0
UniqInverse_EqDeltaProjs.u2 <= diagonal_inverse1.u0
UniqInverse_EqDeltaProjs.u2 <= diagonal_inverse2.u0
UniqInverse_EqDeltaProjs.u2 <= UniqInverse_EqDeltaProjs.u0
UniqInverse_EqDeltaProjs.u2 <= UniqInverse_EqDeltaProjs.u1
[private-mono,fragile,default]
File "./theories/Logic/ExtensionalityFacts.v", line 117, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
FunctExt_iff_EqDeltaProjs.u0 = FunctExt_UniqInverse.u0
FunctExt_iff_EqDeltaProjs.u0 = FunctExt_iff_UniqInverse.u0
FunctExt_iff_EqDeltaProjs.u1 = FunctExt_UniqInverse.u1
FunctExt_iff_EqDeltaProjs.u1 = FunctExt_iff_UniqInverse.u1
FunctExt_iff_EqDeltaProjs.u2 = UniqInverse_EqDeltaProjs.u2
FunctExt_UniqInverse.u2 = UniqInverse_EqDeltaProjs.u0
FunctExt_UniqInverse.u2 = FunctExt_iff_UniqInverse.u2
FunctExt_UniqInverse.u3 = UniqInverse_EqDeltaProjs.u1
FunctExt_UniqInverse.u3 = FunctExt_iff_UniqInverse.u3
[private-mono,fragile,default]
File "./theories/Logic/ExtensionalityFacts.v", line 127, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
FunctExt_BijComp.u2 <= FunctExt_BijComp.u0
FunctExt_BijComp.u3 <= FunctExt_BijComp.u0
FunctExt_BijComp.u4 <= FunctExt_BijComp.u1 [private-mono,fragile,default]
File "./theories/Logic/ExtensionalityFacts.v", line 139, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
FunctExt_iff_UniqInverse.u2 <= action.u1
FunctExt_iff_UniqInverse.u2 <= action.u2
FunctExt_iff_UniqInverse.u2 <= BijComp_FunctExt.u0
FunctExt_iff_UniqInverse.u2 <= BijComp_FunctExt.u2
FunctExt_iff_UniqInverse.u3 <= action.u0
FunctExt_iff_UniqInverse.u3 <= BijComp_FunctExt.u1
FunctExt_iff_UniqInverse.u0 = BijComp_FunctExt.u3
FunctExt_iff_UniqInverse.u1 = BijComp_FunctExt.u4
[private-mono,fragile,default]
File "./theories/Logic/FunctionalExtensionality.v", line 34, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
functional_extensionality.u0 <= functional_extensionality_dep.u0
functional_extensionality.u1 <= functional_extensionality_dep.u1
[private-mono,fragile,default]
File "./theories/Logic/FunctionalExtensionality.v", line 109, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
forall_eq_rect_comp.u0 <= functional_extensionality_dep_good_refl.u0
forall_eq_rect_comp.u1 <= functional_extensionality_dep_good_refl.u1
[private-mono,fragile,default]
File "./theories/Logic/FunctionalExtensionality.v", line 262, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
eta_expansion.u0 <= eta_expansion_dep.u0
eta_expansion.u1 <= eta_expansion_dep.u1 [private-mono,fragile,default]
File "./theories/Logic/PropExtensionalityFacts.v", line 82, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
PredExt_imp_PropFunExt.u1 <= PredExt_imp_PropFunExt.u0
[private-mono,fragile,default]
File "./theories/Logic/PropExtensionalityFacts.v", line 89, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
PropExt_and_PropFunExt_imp_PredExt.u1 <= PropExt_and_PropFunExt_imp_PredExt.u0
[private-mono,fragile,default]
File "./theories/Logic/PropExtensionalityFacts.v", line 95, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
PredExt_imp_PropExt.u0 <= PredExt_imp_PropFunExt.u1
PredExt_imp_PropExt.u0 <= PropExt_and_PropFunExt_iff_PredExt.u0
PredExt_imp_PropExt.u0 <= PropExt_and_PropFunExt_iff_PredExt.u1
PredExt_imp_PropFunExt.u0 <= PropExt_and_PropFunExt_iff_PredExt.u0
PredExt_imp_PropFunExt.u0 <= PropExt_and_PropFunExt_iff_PredExt.u1
PropExt_and_PropFunExt_imp_PredExt.u0 <= PredExt_imp_PropFunExt.u1
PropExt_and_PropFunExt_imp_PredExt.u0 <= PropExt_and_PropFunExt_iff_PredExt.u0
PropExt_and_PropFunExt_iff_PredExt.u0 <= PredExt_imp_PropFunExt.u1
PropExt_and_PropFunExt_iff_PredExt.u1 <= PropExt_and_PropFunExt_iff_PredExt.u0
[private-mono,fragile,default]
File "./theories/Logic/EqdepFacts.v", line 128, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
eq_sigT_eq_dep.u0 <= Coq.Init.Specif.22
eq_sigT_eq_dep.u1 <= Coq.Init.Specif.23 [private-mono,fragile,default]
File "./theories/Logic/EqdepFacts.v", line 142, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
eq_sigT_iff_eq_dep.u0 <= eq_sigT_eq_dep.u0
eq_sigT_iff_eq_dep.u0 <= eq_dep_eq_sigT.u0
eq_sigT_iff_eq_dep.u1 <= eq_sigT_eq_dep.u1
eq_sigT_iff_eq_dep.u1 <= eq_dep_eq_sigT.u1 [private-mono,fragile,default]
File "./theories/Logic/EqdepFacts.v", line 153, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
eq_sig_eq_dep.u0 <= Coq.Init.Specif.16 [private-mono,fragile,default]
File "./theories/Logic/EqdepFacts.v", line 167, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
eq_sig_iff_eq_dep.u0 <= eq_sig_eq_dep.u0
eq_sig_iff_eq_dep.u0 <= eq_dep_eq_sig.u0 [private-mono,fragile,default]
File "./theories/Logic/EqdepFacts.v", line 280, characters 2-104:
Warning: Adding constraints to the global env from Qed body:
eq_rect_eq__eq_dep1_eq.u0 <= Eq_rect_eq.u0
eq_rect_eq__eq_dep1_eq.u0 <= eq_rect_eq_on__eq_dep1_eq_on.u0
[private-mono,fragile,default]
File "./theories/Logic/EqdepFacts.v", line 289, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
eq_rect_eq_on__eq_dep_eq_on.u0 <= eq_rect_eq_on__eq_dep1_eq_on.u0
[private-mono,fragile,default]
File "./theories/Logic/EqdepFacts.v", line 291, characters 2-103:
Warning: Adding constraints to the global env from Qed body:
Eq_dep_eq.u0 <= Eq_rect_eq.u0
Eq_dep_eq.u0 <= eq_rect_eq_on__eq_dep_eq_on.u0 [private-mono,fragile,default]
File "./theories/Logic/EqdepFacts.v", line 345, characters 2-101:
Warning: Adding constraints to the global env from Qed body:
Eq_rect_eq.u0 <= Streicher_K_on__eq_rect_eq_on.u0
[private-mono,fragile,default]
File "./theories/Logic/EqdepFacts.v", line 385, characters 0-68:
Warning: Adding constraints to the global env from Qed body:
UIP_shift.u0 <= UIP_shift_on.u0 [private-mono,fragile,default]
File "./theories/Logic/EqdepFacts.v", line 406, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
Coq.Logic.EqdepFacts.71 <= eq_sigT_eq_dep.u0
eq_dep_eq_on__inj_pair2_on.u0 <= eq_sigT_eq_dep.u1
[private-mono,fragile,default]
File "./theories/Logic/EqdepFacts.v", line 408, characters 1-94:
Warning: Adding constraints to the global env from Qed body:
Inj_dep_pair.u0 <= Eq_dep_eq.u0
Inj_dep_pair.u0 <= eq_dep_eq_on__inj_pair2_on.u0
[private-mono,fragile,default]
File "./theories/Logic/EqdepFacts.v", line 439, characters 0-21:
Warning: Adding constraints to the global env from Qed body:
Coq.Logic.EqdepFacts.80 <= M.eq_rect_eq.u0
M.eq_rect_eq.u1 = eq_rect_eq.u0 [private-mono,fragile,default]
File "./theories/Logic/EqdepFacts.v", line 448, characters 0-43:
Warning: Adding constraints to the global env from Qed body:
Coq.Logic.EqdepFacts.80 <= Coq.Logic.EqdepFacts.46
Eq_rect_eq.u0 = eq_rect_eq.u0
Eq_dep_eq.u0 = eq_dep_eq.u0 [private-mono,fragile,default]
File "./theories/Logic/EqdepFacts.v", line 475, characters 0-54:
Warning: Adding constraints to the global env from Qed body:
inj_pair2.u0 <= Coq.Logic.EqdepFacts.71
inj_pair2.u0 <= Coq.Logic.EqdepFacts.80
Inj_dep_pair.u0 = inj_pair2.u1 [private-mono,fragile,default]
File "./theories/Program/Combinators.v", line 68, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
uncurry_curry.u0 <= functional_extensionality.u0
uncurry_curry.u0 <= functional_extensionality.u1
uncurry_curry.u1 <= functional_extensionality.u0
uncurry_curry.u1 <= functional_extensionality.u1
uncurry_curry.u2 <= functional_extensionality.u0
uncurry_curry.u2 <= functional_extensionality.u1
[private-mono,fragile,default]
File "./theories/Logic/HLevels.v", line 50, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
forall_hprop.u0 <= functional_extensionality_dep.u0
[private-mono,fragile,default]
File "./theories/Logic/HLevels.v", line 87, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
not_hprop.u0 <= functional_extensionality.u0 [private-mono,fragile,default]
File "./theories/Logic/HLevels.v", line 113, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
eq_trans_cancel.u0 <= eq_trans_refl_l.u0 [private-mono,fragile,default]
File "./theories/Logic/HLevels.v", line 138, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
hprop_hprop.u0 <= forall_hprop.u0
hprop_hprop.u0 <= hset_hprop.u0 [private-mono,fragile,default]
File "./theories/Logic/HLevels.v", line 149, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
hprop_hset.u0 <= hset_hOneType.u0
hprop_hset.u0 <= functional_extensionality_dep.u0
[private-mono,fragile,default]
File "./theories/Sets/Relations_1_facts.v", line 65, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Equiv_from_order.u0 <= Equiv_from_preorder.u0 [private-mono,fragile,default]
File "./theories/Sets/Relations_1_facts.v", line 81, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Relations_1.1 <= Equiv_from_preorder.u0
same_relation_is_equivalence.u0 <= contains_is_preorder.u0
[private-mono,fragile,default]
File "./theories/Wellfounded/Well_Ordering.v", line 47, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Wellfounded.Well_Ordering.5 <= Coq.Logic.EqdepFacts.1
Coq.Wellfounded.Well_Ordering.5 <= Coq.Logic.EqdepFacts.2
Coq.Wellfounded.Well_Ordering.5 <= sigT.u0
Coq.Wellfounded.Well_Ordering.5 <= sigT.u1
Coq.Wellfounded.Well_Ordering.5 <= Coq.Init.Specif.22
Coq.Wellfounded.Well_Ordering.5 <= Coq.Init.Specif.23
Coq.Wellfounded.Well_Ordering.6 <= Coq.Logic.EqdepFacts.2
Coq.Wellfounded.Well_Ordering.6 <= sigT.u1
Coq.Wellfounded.Well_Ordering.6 <= Coq.Init.Specif.23
[private-mono,fragile,default]
File "./theories/Wellfounded/Well_Ordering.v", line 72, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Wellfounded.Well_Ordering.15 <= well_founded_induction_type.u0
[private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 138, characters 0-45:
Warning: Adding constraints to the global env from Qed body:
eq_proofs_unicity.u0 <= Coq.Logic.Eqdep_dec.1 [private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 142, characters 0-33:
Warning: Adding constraints to the global env from Qed body:
K_dec.u0 <= Coq.Logic.Eqdep_dec.1 [private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 147, characters 0-42:
Warning: Adding constraints to the global env from Qed body:
inj_right_pair.u0 <= Coq.Logic.Eqdep_dec.1 [private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 158, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
K_dec_type.u0 <= K_dec.u0 [private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 174, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
eq_rect_eq_dec.u0 <= K_dec_type.u0
eq_rect_eq_dec.u0 <= Coq.Logic.EqdepFacts.46
Eq_rect_eq.u0 = eq_rect_eq_dec.u1 [private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 181, characters 0-72:
Warning: Adding constraints to the global env from Qed body:
eq_dep_eq_dec.u0 <= eq_rect_eq_dec.u0
eq_dep_eq_dec.u0 <= Coq.Logic.EqdepFacts.46
Eq_dep_eq.u0 = eq_dep_eq_dec.u1 [private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 187, characters 0-64:
Warning: Adding constraints to the global env from Qed body:
UIP_dec.u0 <= eq_dep_eq_dec.u0
UIP_dec.u0 <= Coq.Logic.EqdepFacts.46 [private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 214, characters 2-30:
Warning: Adding constraints to the global env from Qed body:
U.u0 <= eq_rect_eq_dec.u0
eq_rect_eq_dec.u1 = eq_rect_eq.u0 [private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 220, characters 2-45:
Warning: Adding constraints to the global env from Qed body:
Eq_dep_eq.u0 = eq_dep_eq.u0 [private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 243, characters 2-42:
Warning: Adding constraints to the global env from Qed body:
U.u0 <= Coq.Logic.EqdepFacts.71
Inj_dep_pair.u0 = inj_pairT2.u0 [private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 255, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
U.u0 <= inj_right_pair.u0 [private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 283, characters 2-30:
Warning: Adding constraints to the global env from Qed body:
eq_rect_eq_dec.u1 = eq_rect_eq.u0 [private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 289, characters 2-45:
Warning: Adding constraints to the global env from Qed body:
Eq_dep_eq.u0 = eq_dep_eq.u0 [private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 319, characters 2-43:
Warning: Adding constraints to the global env from Qed body:
Inj_dep_pair.u0 = inj_pair2.u0 [private-mono,fragile,default]
File "./theories/Logic/Eqdep_dec.v", line 338, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
inj_pair2_eq_dec.u0 <= eq_rect_eq_dec.u0
inj_pair2_eq_dec.u0 <= Coq.Logic.EqdepFacts.46
inj_pair2_eq_dec.u0 <= Coq.Logic.EqdepFacts.71
Inj_dep_pair.u0 = inj_pair2_eq_dec.u1 [private-mono,fragile,default]
File "./theories/Sets/Finite_sets.v", line 81, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Finite_sets.2 <= Coq.Sets.Constructive_sets.1
[private-mono,fragile,default]
File "./theories/Wellfounded/Disjoint_Union.v", line 30, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Wellfounded.Disjoint_Union.1 <= eq.u0 [private-mono,fragile,default]
File "./theories/Program/Wf.v", line 149, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Fix_F_sub_rect.u0 <= well_founded_induction_type.u0
Fix_F_sub_rect.u0 <= eq_rect_r.u0 [private-mono,fragile,default]
File "./theories/Program/Wf.v", line 210, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Fix_sub_rect.u0 <= Coq.Init.Logic.10
Fix_sub_rect.u0 <= Fix_F_sub_rect.u0 [private-mono,fragile,default]
File "./theories/Program/Wf.v", line 250, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fix_sub_eq_ext.u0 <= eq.u0
fix_sub_eq_ext.u0 <= functional_extensionality_dep.u0
fix_sub_eq_ext.u1 <= functional_extensionality_dep.u1
[private-mono,fragile,default]
File "./theories/Logic/JMeq.v", line 46, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
JMeq.u1 <= JMeq.u0 [private-mono,fragile,default]
File "./theories/Logic/JMeq.v", line 66, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
JMeq_eq.u0 < sigT.u0
JMeq_eq.u0 < eq.u0
JMeq_eq.u0 < inj_pair2.u0
JMeq_eq.u0 <= sigT.u1
JMeq_eq.u0 <= inj_pair2.u1
JMeq.u1 = JMeq_eq.u0 [private-mono,fragile,default]
File "./theories/Logic/JMeq.v", line 92, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
JMeq_ind_r.u0 <= JMeq_sym.u0
JMeq_ind_r.u0 <= JMeq_sym.u1 [private-mono,fragile,default]
File "./theories/Logic/JMeq.v", line 98, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
JMeq_rec_r.u0 <= JMeq_sym.u0
JMeq_rec_r.u0 <= JMeq_sym.u1 [private-mono,fragile,default]
File "./theories/Logic/JMeq.v", line 104, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
JMeq_rect_r.u0 <= JMeq_sym.u0
JMeq_rect_r.u0 <= JMeq_sym.u1 [private-mono,fragile,default]
File "./theories/Logic/JMeq.v", line 123, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
JMeq.u1 <= JMeq_eq_dep_id.u2 [private-mono,fragile,default]
File "./theories/Logic/JMeq.v", line 130, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
eq_dep_id_JMeq.u2 <= JMeq.u1 [private-mono,fragile,default]
File "./theories/Sets/Relations_2_facts.v", line 58, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Rstar_contains_Rplus.u0 <= Rstar_contains_R.u0 [private-mono,fragile,default]
File "./theories/Sets/Relations_2_facts.v", line 85, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Rstar_equiv_Rstar1.u0 <= Rstar_contains_R.u0
Rstar_equiv_Rstar1.u0 <= Rstar_transitive.u0 [private-mono,fragile,default]
File "./theories/Sets/Relations_2_facts.v", line 96, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Rsym_imp_Rstarsym.u0 <= Rstar_transitive.u0 [private-mono,fragile,default]
File "./theories/Sets/Relations_2_facts.v", line 106, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Sstar_contains_Rstar.u0 <= Rstar_transitive.u0 [private-mono,fragile,default]
File "./theories/Sets/Relations_2_facts.v", line 115, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
star_monotone.u0 <= Rstar_contains_R.u0
star_monotone.u0 <= Sstar_contains_Rstar.u0 [private-mono,fragile,default]
File "./theories/Sets/Relations_2_facts.v", line 130, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
RstarRplus_RRstar.u0 <= Rstar_contains_Rplus.u0
RstarRplus_RRstar.u0 <= Rstar_transitive.u0 [private-mono,fragile,default]
File "./theories/Wellfounded/Union.v", line 64, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Wellfounded.Union.1 <= Coq.Wellfounded.Transitive_Closure.1
[private-mono,fragile,default]
File "./theories/Program/Equality.v", line 179, characters 23-27:
Warning: Adding constraints to the global env from Qed body:
inj_pairT2_refl.u1 <= Coq.Logic.EqdepFacts.80 [private-mono,fragile,default]
File "./theories/Sets/Powerset.v", line 95, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Ensembles.1 <= Coq.Sets.Partial_Order.4
[private-mono,fragile,default]
File "./theories/Sets/Powerset.v", line 113, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Ensembles.1 <= cong_transitive_same_relation.u0
[private-mono,fragile,default]
File "./theories/Sets/Relations_3_facts.v", line 76, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Strong_confluence.u0 <= Lemma1.u0 [private-mono,fragile,default]
File "./theories/Sets/Relations_3_facts.v", line 172, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Newman.u0 <= Rstar_imp_coherent.u0
Newman.u0 <= coherent_symmetric.u0
Newman.u0 <= Rstar_transitive.u0
Newman.u0 <= Rstar_cases.u0 [private-mono,fragile,default]
File "./theories/Wellfounded/Lexicographic_Product.v", line 93, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Wellfounded.Lexicographic_Product.3 <= Coq.Wellfounded.Inclusion.1
Coq.Wellfounded.Lexicographic_Product.3 <= Coq.Wellfounded.Inverse_Image.1
Coq.Wellfounded.Lexicographic_Product.3 <= Coq.Wellfounded.Lexicographic_Product.1
Coq.Wellfounded.Lexicographic_Product.4 <= Coq.Wellfounded.Inclusion.1
Coq.Wellfounded.Lexicographic_Product.4 <= Coq.Wellfounded.Inverse_Image.1
Coq.Wellfounded.Lexicographic_Product.4 <= Coq.Wellfounded.Lexicographic_Product.2
[private-mono,fragile,default]
File "./theories/Program/Subset.v", line 81, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
subset_eq.u0 < eq.u0 [private-mono,fragile,default]
File "./theories/Program/Subset.v", line 103, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
match_eq_rewrite.u0 <= subset_eq.u0 [private-mono,fragile,default]
File "./theories/ssr/ssreflect.v", line 443, characters 22-26:
Warning: Adding constraints to the global env from Qed body:
unlock_with.u0 <= unlock.u0 [private-mono,fragile,default]
File "./theories/ssr/ssreflect.v", line 469, characters 18-22:
Warning: Adding constraints to the global env from Qed body:
ssr_congr_arrow.u0 <= eq_rect_r.u0
ssr_congr_arrow.u1 <= eq_rect_r.u0 [private-mono,fragile,default]
File "./theories/Sets/Powerset_facts.v", line 45, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Powerset_facts.1 <= Coq.Sets.Powerset.1
[private-mono,fragile,default]
File "./theories/Sets/Powerset_facts.v", line 152, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Powerset_facts.1 < eq.u0 [private-mono,fragile,default]
File "./theories/Sets/Powerset_facts.v", line 198, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Powerset_facts.1 <= Coq.Sets.Constructive_sets.1
[private-mono,fragile,default]
File "./theories/Sets/Powerset_facts.v", line 281, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Disjoint_Intersection.u0 <= Coq.Sets.Powerset.1
[private-mono,fragile,default]
File "./theories/Sets/Powerset_facts.v", line 287, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Intersection_Empty_set_l.u0 <= Coq.Sets.Powerset.1
[private-mono,fragile,default]
File "./theories/Sets/Powerset_facts.v", line 293, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Intersection_Empty_set_r.u0 <= Coq.Sets.Powerset.1
[private-mono,fragile,default]
File "./theories/Sets/Powerset_facts.v", line 301, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Seminus_Empty_set_l.u0 <= Coq.Sets.Powerset.1 [private-mono,fragile,default]
File "./theories/Sets/Powerset_facts.v", line 309, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Seminus_Empty_set_r.u0 <= Coq.Sets.Constructive_sets.1
[private-mono,fragile,default]
File "./theories/Sets/Powerset_facts.v", line 318, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Setminus_Union_l.u0 <= Coq.Sets.Constructive_sets.1
[private-mono,fragile,default]
File "./theories/Sets/Powerset_facts.v", line 329, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Setminus_Union_r.u0 <= Coq.Sets.Constructive_sets.1
[private-mono,fragile,default]
File "./theories/Sets/Powerset_facts.v", line 340, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Setminus_Disjoint_noop.u0 <= Coq.Sets.Constructive_sets.1
[private-mono,fragile,default]
File "./theories/Sets/Powerset_facts.v", line 349, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Setminus_Included_empty.u0 <= Coq.Sets.Powerset.1
[private-mono,fragile,default]
File "./theories/ssr/ssrfun.v", line 564, characters 70-74:
Warning: Adding constraints to the global env from Qed body:
all_tag.u1 <= Coq.Init.Specif.22
all_tag.u2 <= Coq.Init.Specif.23 [private-mono,fragile,default]
File "./theories/ssr/ssrfun.v", line 569, characters 50-54:
Warning: Adding constraints to the global env from Qed body:
all_tag2.u0 <= all_pair.u0
all_tag2.u0 <= sigT.u0
all_tag2.u0 <= sigT.u1
all_tag2.u0 <= prod.u0
all_tag2.u0 <= prod.u1
all_tag2.u0 <= all_tag.u0
all_tag2.u1 <= sigT.u0
all_tag2.u1 <= tag_of_tag2.u0
all_tag2.u1 <= all_tag.u1
all_tag2.u2 <= sigT.u1
all_tag2.u2 <= all_pair.u1
all_tag2.u2 <= prod.u0
all_tag2.u2 <= tag_of_tag2.u1
all_tag2.u2 <= all_tag.u2
all_tag2.u3 <= sigT.u1
all_tag2.u3 <= all_pair.u2
all_tag2.u3 <= prod.u1
all_tag2.u3 <= tag_of_tag2.u2
all_tag2.u3 <= all_tag.u2 [private-mono,fragile,default]
File "./theories/ssr/ssrfun.v", line 601, characters 38-42:
Warning: Adding constraints to the global env from Qed body:
all_sig.u0 <= sigT.u0
all_sig.u0 <= all_tag.u0
all_sig.u1 <= sigT.u0
all_sig.u1 <= all_tag.u1
all_sig.u1 <= tag_of_sig.u0 [private-mono,fragile,default]
File "./theories/ssr/ssrfun.v", line 606, characters 50-54:
Warning: Adding constraints to the global env from Qed body:
all_sig2.u0 <= sig.u0
all_sig2.u0 <= all_pair.u0
all_sig2.u0 <= all_sig.u0
all_sig2.u1 <= sig.u0
all_sig2.u1 <= sig_of_sig2.u0
all_sig2.u1 <= all_sig.u1 [private-mono,fragile,default]
File "./theories/ssr/ssrfun.v", line 677, characters 39-43:
Warning: Adding constraints to the global env from Qed body:
Coq.ssr.ssrfun.265 <= nary_congruence_statement.u0
Coq.ssr.ssrfun.265 <= nary_congruence_statement.u1
[private-mono,fragile,default]
File "./theories/ssr/ssrfun.v", line 763, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.ssr.ssrfun.363 <= Coq.ssr.ssrfun.316 [private-mono,fragile,default]
File "./theories/Classes/Morphisms.v", line 654, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Relations.Relation_Definitions.1 <= Coq.Classes.Morphisms.31
Coq.Classes.Morphisms.95 <= Coq.Classes.Morphisms.31
Coq.Classes.Morphisms.95 <= proper_proper.u0 [private-mono,fragile,default]
File "./theories/Classes/Morphisms.v", line 746, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
PartialOrder_proper.u0 <= proper_sym_impl_iff_2.u0
PartialOrder_proper.u0 <= proper_sym_impl_iff_2.u1
[private-mono,fragile,default]
File "./theories/Classes/Morphisms.v", line 763, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
PartialOrder_StrictOrder.u0 <= Coq.Classes.Morphisms.51
PartialOrder_StrictOrder.u0 <= PartialOrder_proper.u0
[private-mono,fragile,default]
File "./theories/Classes/Morphisms.v", line 781, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
StrictOrder_PreOrder.u0 <= Coq.Classes.Morphisms.51
[private-mono,fragile,default]
File "./theories/Classes/CEquivalence.v", line 153, characters 23-27:
Warning: Adding constraints to the global env from Qed body:
pointwise_reflexive.u0 = pointwise_symmetric.u0
pointwise_reflexive.u0 = pointwise_transitive.u0
pointwise_reflexive.u1 = pointwise_symmetric.u1
pointwise_reflexive.u1 = pointwise_transitive.u1
pointwise_reflexive.u2 = pointwise_symmetric.u2
pointwise_reflexive.u2 = pointwise_transitive.u2
pointwise_reflexive.u3 = pointwise_symmetric.u3
pointwise_reflexive.u3 = pointwise_transitive.u3
pointwise_reflexive.u4 = pointwise_symmetric.u4
pointwise_reflexive.u4 = pointwise_transitive.u4
pointwise_equivalence.u0 = pointwise_reflexive.u0
pointwise_equivalence.u1 = pointwise_reflexive.u1
pointwise_equivalence.u2 = pointwise_reflexive.u2
pointwise_equivalence.u3 = pointwise_reflexive.u3
pointwise_equivalence.u4 = pointwise_reflexive.u4
[private-mono,fragile,default]
File "./theories/Classes/SetoidClass.v", line 98, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
nequiv_equiv_trans.u0 <= setoid_sym.u0
nequiv_equiv_trans.u0 <= setoid_trans.u0 [private-mono,fragile,default]
File "./theories/Classes/SetoidClass.v", line 106, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
equiv_nequiv_trans.u0 <= setoid_sym.u0
equiv_nequiv_trans.u0 <= setoid_trans.u0 [private-mono,fragile,default]
File "./theories/Classes/Morphisms_Prop.v", line 96, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Acc_pt_morphism.u0 <= Coq.Classes.Morphisms.51
Acc_pt_morphism.u0 <= proper_sym_impl_iff.u0 [private-mono,fragile,default]
File "./theories/Classes/Morphisms_Prop.v", line 110, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Relations.Relation_Definitions.1 <= proper_sym_impl_iff_2.u0
Acc_rel_morphism.u0 <= proper_sym_impl_iff_2.u1
[private-mono,fragile,default]
File "./theories/Classes/Morphisms_Prop.v", line 119, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
well_founded_morphism.u0 <= all_iff_morphism_obligation_1.u0
well_founded_morphism.u0 <= all.u0
well_founded_morphism.u0 <= Acc_rel_morphism.u0
[private-mono,fragile,default]
File "./theories/Classes/Equivalence.v", line 154, characters 23-27:
Warning: Adding constraints to the global env from Qed body:
pointwise_equivalence.u0 <= pointwise_reflexive.u0
pointwise_equivalence.u0 <= pointwise_symmetric.u0
pointwise_equivalence.u0 <= pointwise_transitive.u0
pointwise_equivalence.u1 <= pointwise_reflexive.u1
pointwise_equivalence.u1 <= pointwise_symmetric.u1
pointwise_equivalence.u1 <= pointwise_transitive.u1
[private-mono,fragile,default]
File "./theories/Structures/Equalities.v", line 201, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= Coq.Classes.Morphisms.51 [private-mono,fragile,default]
File "./theories/Structures/Orders.v", line 357, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= proper_sym_impl_iff_2.u1 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 793, characters 57-61:
Warning: Adding constraints to the global env from Qed body:
unless_sym.u0 <= impliesP.u0
unless_sym.u0 <= unlessL.u1
unless_sym.u0 <= unlessR.u0
unless_sym.u1 <= impliesP.u0
unless_sym.u1 <= unlessL.u0
unless_sym.u1 <= unlessR.u1 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 799, characters 75-79:
Warning: Adding constraints to the global env from Qed body:
bind_unless.u0 <= impliesP.u0
bind_unless.u0 <= unlessL.u0
bind_unless.u1 <= impliesP.u0
bind_unless.u1 <= unlessL.u1
bind_unless.u1 <= unlessR.u0
bind_unless.u2 <= unlessL.u1 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 802, characters 74-78:
Warning: Adding constraints to the global env from Qed body:
unless_contra.u0 <= impliesP.u0
unless_contra.u0 <= unlessL.u0
unless_contra.u0 <= unlessR.u1 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 839, characters 75-79:
Warning: Adding constraints to the global env from Qed body:
classic_sigW.u0 <= classicW.u0
classic_sigW.u0 <= classic_bind.u0
classic_sigW.u0 <= classic_bind.u1 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 1727, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
all_tag_cond_dep.u0 <= all_tag.u0
all_tag_cond_dep.u1 <= all_tag.u1
all_tag_cond_dep.u2 <= Coq.Init.Logic.2
all_tag_cond_dep.u2 <= all_tag.u2 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 1732, characters 46-50:
Warning: Adding constraints to the global env from Qed body:
all_tag_cond.u0 <= all_tag_cond_dep.u0
all_tag_cond.u1 <= all_tag_cond_dep.u1
all_tag_cond.u2 <= all_tag_cond_dep.u2 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 1737, characters 57-61:
Warning: Adding constraints to the global env from Qed body:
all_sig_cond_dep.u0 <= sigT.u0
all_sig_cond_dep.u0 <= all_tag_cond_dep.u0
all_sig_cond_dep.u1 <= sigT.u0
all_sig_cond_dep.u1 <= tag_of_sig.u0
all_sig_cond_dep.u1 <= all_tag_cond_dep.u1 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 1742, characters 46-50:
Warning: Adding constraints to the global env from Qed body:
all_sig_cond.u0 <= all_sig_cond_dep.u0
all_sig_cond.u1 <= all_sig_cond_dep.u1 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 1749, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
all_sig2_cond.u0 <= sig.u0
all_sig2_cond.u0 <= all_sig_cond.u0
all_sig2_cond.u1 <= sig.u0
all_sig2_cond.u1 <= sig_of_sig2.u0
all_sig2_cond.u1 <= all_sig_cond.u1 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 2015, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
predArgType.u0 <= Coq.ssr.ssrbool.1414 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 2144, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
ocan_in_comp.u1 <= Coq.ssr.ssrbool.1414 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 2172, characters 46-50:
Warning: Adding constraints to the global env from Qed body:
sub_in2.u0 <= predArgType.u0 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 2176, characters 47-51:
Warning: Adding constraints to the global env from Qed body:
sub_in3.u0 <= predArgType.u0 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 2181, characters 48-52:
Warning: Adding constraints to the global env from Qed body:
sub_in12.u0 <= predArgType.u0
sub_in12.u1 <= predArgType.u0 [private-mono,fragile,default]
File "./theories/ssr/ssrbool.v", line 2186, characters 48-52:
Warning: Adding constraints to the global env from Qed body:
sub_in21.u0 <= predArgType.u0
sub_in21.u1 <= predArgType.u0 [private-mono,fragile,default]
File "./theories/Numbers/NatInt/NZOrder.v", line 401, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= all_iff_morphism_obligation_1.u0
t.u0 <= all.u0 [private-mono,fragile,default]
File "./theories/Numbers/NatInt/NZOrder.v", line 440, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= Acc_pt_morphism.u0 [private-mono,fragile,default]
File "./theories/Numbers/NatInt/NZAddOrder.v", line 171, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= ex_iff_morphism_obligation_1.u0 [private-mono,fragile,default]
File "./theories/Numbers/NatInt/NZSqrt.v", line 248, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= default_relation.u0
t.u0 <= equivalence_default.u0 [private-mono,fragile,default]
File "./theories/Numbers/NatInt/NZSqrt.v", line 446, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= rewrite_relation_eq_dom.u0
t.u0 <= rewrite_relation_eq_dom.u1 [private-mono,fragile,default]
File "./theories/Numbers/NatInt/NZLog.v", line 371, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= default_relation.u0
t.u0 <= equivalence_default.u0 [private-mono,fragile,default]
File "./theories/Numbers/NatInt/NZLog.v", line 504, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= rewrite_relation_eq_dom.u0
t.u0 <= rewrite_relation_eq_dom.u1 [private-mono,fragile,default]
File "./theories/Numbers/Natural/Abstract/NIso.v", line 33, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
N2.t.u0 <= N2.recursion_wd.u0 [private-mono,fragile,default]
File "./theories/Numbers/Natural/Abstract/NIso.v", line 38, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
N2.t.u0 <= N2.recursion_0.u0 [private-mono,fragile,default]
File "./theories/Numbers/Natural/Abstract/NIso.v", line 46, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
N2.t.u0 <= N2.recursion_succ.u0 [private-mono,fragile,default]
File "./theories/Numbers/Natural/Abstract/NStrongRec.v", line 61, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= recursion_wd.u0
Coq.Numbers.Natural.Abstract.NStrongRec.1 <= recursion_wd.u0
[private-mono,fragile,default]
File "./theories/Numbers/Natural/Abstract/NStrongRec.v", line 79, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= recursion_0.u0
Coq.Numbers.Natural.Abstract.NStrongRec.1 <= recursion_0.u0
[private-mono,fragile,default]
File "./theories/Numbers/Natural/Abstract/NStrongRec.v", line 87, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= recursion_succ.u0
Coq.Numbers.Natural.Abstract.NStrongRec.1 <= recursion_succ.u0
Coq.Numbers.Natural.Abstract.NStrongRec.1 <= rewrite_relation_eq_dom.u0
Coq.Numbers.Natural.Abstract.NStrongRec.1 <= rewrite_relation_eq_dom.u1
Coq.Numbers.Natural.Abstract.NStrongRec.1 <= Coq.Classes.Morphisms.51
Coq.Relations.Relation_Definitions.1 <= rewrite_relation_eq_dom.u0
Coq.Relations.Relation_Definitions.1 <= rewrite_relation_eq_dom.u1
Coq.Relations.Relation_Definitions.1 <= Coq.Classes.Morphisms.51
[private-mono,fragile,default]
File "./theories/Numbers/Natural/Abstract/NGcd.v", line 176, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= prod.u0
t.u0 <= prod.u1
t.u0 <= measure_induction.u0 [private-mono,fragile,default]
File "./theories/Numbers/Natural/Abstract/NBits.v", line 55, characters 21-25:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= eq_rewrite_relation.u0 [private-mono,fragile,default]
File "./theories/Arith/PeanoNat.v", line 521, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_swap.u0 <= iter_swap_gen.u0
iter_swap.u0 <= iter_swap_gen.u1 [private-mono,fragile,default]
File "./theories/Arith/PeanoNat.v", line 535, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_succ_r.u0 <= iter_swap.u0
iter_succ_r.u0 <= iter_succ.u0 [private-mono,fragile,default]
File "./theories/Arith/PeanoNat.v", line 572, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_invariant.u0 <= iter_ind.u0 [private-mono,fragile,default]
File "./theories/Arith/PeanoNat.v", line 1228, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
OddT_EvenT_rect.u0 <= Coq.Init.Logic.2 [private-mono,fragile,default]
File "./theories/Arith/PeanoNat.v", line 1237, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
EvenT_OddT_rect.u0 <= OddT_EvenT_rect.u0
EvenT_OddT_rect.u1 <= OddT_EvenT_rect.u1 [private-mono,fragile,default]
File "./theories/Sets/Multiset.v", line 113, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Multiset.1 <= Coq.Sets.Permut.1 [private-mono,fragile,default]
File "./theories/Sets/Multiset.v", line 176, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Multiset.1 <= Coq.Classes.Morphisms.51
[private-mono,fragile,default]
File "./theories/Numbers/NatInt/NZDomain.v", line 57, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= nat_rect_wd.u0
t.u0 <= nat_rect_succ_r.u0 [private-mono,fragile,default]
File "./theories/Logic/ClassicalFacts.v", line 669, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
IndependenceOfGeneralPremises.u0 = DrinkerParadox.u0
[private-mono,fragile,default]
File "./theories/Vectors/Fin.v", line 231, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
case_L_R'.u0 < Coq.Init.Datatypes.9
case_L_R'.u0 <= caseS'.u0 [private-mono,fragile,default]
File "./theories/Vectors/Fin.v", line 239, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
case_L_R.u0 <= case_L_R'.u0 [private-mono,fragile,default]
File "./theories/Logic/ClassicalUniqueChoice.v", line 45, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
unique_choice.u0 <= dependent_unique_choice.u0
unique_choice.u1 <= dependent_unique_choice.u1 [private-mono,fragile,default]
File "./theories/Sets/Classical_sets.v", line 46, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Classical_sets.1 <= Coq.Logic.Classical_Pred_Type.1
Coq.Sets.Classical_sets.1 <= ex.u0 [private-mono,fragile,default]
File "./theories/Sets/Classical_sets.v", line 53, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Classical_sets.1 <= Coq.Sets.Constructive_sets.1
[private-mono,fragile,default]
File "./theories/PArith/BinPos.v", line 396, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
eq_dep_eq_dec.u1 = eq_dep_eq_positive.u0 [private-mono,fragile,default]
File "./theories/PArith/BinPos.v", line 427, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
peano_equiv.u0 <= peano_rect_succ.u0 [private-mono,fragile,default]
File "./theories/PArith/BinPos.v", line 601, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_swap.u0 <= iter_swap_gen.u0
iter_swap.u0 <= iter_swap_gen.u1 [private-mono,fragile,default]
File "./theories/PArith/BinPos.v", line 609, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_succ.u0 <= iter_swap.u0 [private-mono,fragile,default]
File "./theories/PArith/BinPos.v", line 616, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_succ_r.u0 <= iter_swap.u0
iter_succ_r.u0 <= iter_succ.u0 [private-mono,fragile,default]
File "./theories/PArith/BinPos.v", line 625, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_add.u0 <= iter_succ.u0 [private-mono,fragile,default]
File "./theories/PArith/BinPos.v", line 634, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_ind.u0 <= iter_succ.u0 [private-mono,fragile,default]
File "./theories/PArith/BinPos.v", line 642, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_invariant.u0 <= iter_ind.u0 [private-mono,fragile,default]
File "./theories/Sets/Powerset_Classical_facts.v", line 58, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Powerset_Classical_facts.1 <= Coq.Sets.Classical_sets.1
Coq.Sets.Powerset_Classical_facts.1 <= Coq.Sets.Powerset_facts.1
[private-mono,fragile,default]
File "./theories/Sets/Powerset_Classical_facts.v", line 154, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Ensembles.1 <= Coq.Sets.Constructive_sets.1
[private-mono,fragile,default]
File "./theories/Sets/Powerset_Classical_facts.v", line 258, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Powerset_Classical_facts.1 <= setcover_intro.u0
[private-mono,fragile,default]
File "./theories/PArith/Pnat.v", line 206, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
inj_iter.u0 <= iter_succ.u0 [private-mono,fragile,default]
File "./theories/Sets/Finite_sets_facts.v", line 61, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Finite_sets_facts.1 <= Coq.Sets.Powerset_facts.1
[private-mono,fragile,default]
File "./theories/Sets/Finite_sets_facts.v", line 89, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Finite_sets_facts.1 <= Coq.Sets.Powerset_Classical_facts.1
[private-mono,fragile,default]
File "./theories/Sets/Finite_sets_facts.v", line 102, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Finite_sets_facts.1 <= Coq.Sets.Finite_sets.2
[private-mono,fragile,default]
File "./theories/Sets/Image.v", line 77, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Image.1 <= Coq.Sets.Powerset.1 [private-mono,fragile,default]
File "./theories/Sets/Image.v", line 87, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Image.1 <= Coq.Sets.Finite_sets_facts.1
[private-mono,fragile,default]
File "./theories/Sets/Infinite_sets.v", line 61, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Infinite_sets.3 <= Coq.Sets.Classical_sets.1
[private-mono,fragile,default]
File "./theories/Sets/Infinite_sets.v", line 101, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sets.Infinite_sets.3 <= Coq.Sets.Finite_sets_facts.1
[private-mono,fragile,default]
File "./theories/NArith/BinNat.v", line 140, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
peano_rect_succ.u0 <= Pos.peano_rect_succ.u0 [private-mono,fragile,default]
File "./theories/NArith/BinNat.v", line 179, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
recursion_wd.u0 <= peano_rect_succ.u0 [private-mono,fragile,default]
File "./theories/NArith/BinNat.v", line 191, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
recursion_succ.u0 <= peano_rect_succ.u0 [private-mono,fragile,default]
File "./theories/NArith/BinNat.v", line 993, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_swap_gen.u0 <= Pos.iter_swap_gen.u0
iter_swap_gen.u1 <= Pos.iter_swap_gen.u1 [private-mono,fragile,default]
File "./theories/NArith/BinNat.v", line 1000, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_swap.u0 <= iter_swap_gen.u0
iter_swap.u0 <= iter_swap_gen.u1 [private-mono,fragile,default]
File "./theories/NArith/BinNat.v", line 1008, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_succ.u0 <= Pos.iter_succ.u0 [private-mono,fragile,default]
File "./theories/NArith/BinNat.v", line 1015, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_succ_r.u0 <= iter_swap.u0
iter_succ_r.u0 <= iter_succ.u0 [private-mono,fragile,default]
File "./theories/NArith/BinNat.v", line 1023, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_add.u0 <= iter_succ.u0 [private-mono,fragile,default]
File "./theories/NArith/BinNat.v", line 1032, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_ind.u0 <= iter_succ.u0 [private-mono,fragile,default]
File "./theories/NArith/BinNat.v", line 1040, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_invariant.u0 <= iter_ind.u0 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 90, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.13 <= Coq.Init.Datatypes.51 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 142, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.13 < eq.u0 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 215, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.13 <= app_eq_app.u0 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 515, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.54 <= Coq.Classes.Morphisms.1
Coq.Lists.List.54 <= Coq.Classes.RelationClasses.1
Coq.Lists.List.54 <= Morphisms.rewrite_relation_eq_dom.u0
Coq.Lists.List.54 <= Morphisms.rewrite_relation_eq_dom.u1
Coq.Lists.List.54 <= Morphisms.eq_rewrite_relation.u0
Coq.Lists.List.54 <= Coq.Classes.Morphisms.51 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 525, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.54 < eq.u0 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 737, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.54 <= eq_rect_r.u0
Coq.Lists.List.54 <= Coq.Init.Datatypes.51 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 752, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.54 <= Coq.Lists.List.13 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 966, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.280 <= Coq.Lists.List.13 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 1347, characters 53-57:
Warning: Adding constraints to the global env from Qed body:
map_ext_in_iff.u0 <= map_ext_in.u0
map_ext_in_iff.u0 <= ext_in_map.u0
map_ext_in_iff.u1 <= map_ext_in.u1
map_ext_in_iff.u1 <= ext_in_map.u1 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 1355, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
map_ext.u0 <= map_ext_in.u0
map_ext.u1 <= map_ext_in.u1 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 1363, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
flat_map_ext.u0 <= map_ext.u0
flat_map_ext.u1 <= map_ext.u1 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 1403, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fold_left_S_O.u0 <= Coq.Lists.List.13
fold_left_S_O.u0 <= Coq.Lists.List.280 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 1429, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_right_app.u0 <= eq.u0 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 1439, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_left_rev_right.u0 <= fold_right_app.u0
fold_left_rev_right.u1 <= fold_right_app.u1 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 1712, characters 4-8:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.494 <= map_ext_in_iff.u0 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 1718, characters 4-8:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.494 <= map_ext.u0 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 2038, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.524 <= Coq.Lists.List.13 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 2450, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.644 < eq.u0 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 2467, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.644 <= Coq.Lists.List.13 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 2652, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.677 <= Morphisms_Prop.all_iff_morphism_obligation_1.u0
Coq.Lists.List.677 <= all.u0 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 3013, characters 4-8:
Warning: Adding constraints to the global env from Qed body:
Forall_rect.u0 <= Coq.Init.Datatypes.51 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 3047, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.775 <= map_ext_in.u0
map_ext_Forall.u0 <= map_ext_in.u1 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 3165, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Exists_flat_map.u0 <= Exists_map.u0
Exists_flat_map.u1 <= Exists_map.u1
Exists_flat_map.u1 <= Exists_concat.u0 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 3187, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Forall_flat_map.u0 <= Forall_map.u0
Forall_flat_map.u1 <= Forall_map.u1
Forall_flat_map.u1 <= Forall_concat.u0 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 3235, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
notin_flat_map_Forall.u0 <= in_flat_map_Exists.u0
notin_flat_map_Forall.u1 <= in_flat_map_Exists.u1
[private-mono,fragile,default]
File "./theories/Lists/List.v", line 3265, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.914 <= eq.u0 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 3454, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.List.980 < eq.u0 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 3608, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
length_flat_map.u0 <= map_map.u0
length_flat_map.u1 <= map_map.u1
length_flat_map.u1 <= length_concat.u0 [private-mono,fragile,default]
File "./theories/Lists/List.v", line 3617, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
flat_map_constant_length.u0 <= length_flat_map.u0
flat_map_constant_length.u1 <= length_flat_map.u1
[private-mono,fragile,default]
File "./theories/Lists/List.v", line 3626, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
length_list_power.u0 <= flat_map_constant_length.u0
length_list_power.u0 <= flat_map_constant_length.u1
length_list_power.u1 <= flat_map_constant_length.u0
length_list_power.u1 <= flat_map_constant_length.u1
[private-mono,fragile,default]
File "./theories/Logic/WeakFan.v", line 89, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Y_approx.u0 <= Y_unique.u0 [private-mono,fragile,default]
File "./theories/Sorting/Sorted.v", line 60, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.Sorted.1 <= eq.u0 [private-mono,fragile,default]
File "./theories/Sorting/Sorted.v", line 78, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Sorted_rect.u0 <= Coq.Init.Logic.4
Sorted_rect.u0 <= Coq.Init.Datatypes.51 [private-mono,fragile,default]
File "./theories/Sorting/Sorted.v", line 116, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
StronglySorted_rec.u0 <= StronglySorted_rect.u0
[private-mono,fragile,default]
File "./theories/NArith/Nnat.v", line 160, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
inj_iter.u0 <= Pos2Nat.inj_iter.u0 [private-mono,fragile,default]
File "./theories/NArith/Nnat.v", line 254, characters 40-44:
Warning: Adding constraints to the global env from Qed body:
inj_iter.u0 <= N2Nat.inj_iter.u0 [private-mono,fragile,default]
File "./theories/micromega/Refl.v", line 113, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
make_conj_app.u0 <= make_conj_cons.u0 [private-mono,fragile,default]
File "./theories/micromega/Refl.v", line 130, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
make_conj_rapp.u0 <= make_conj_cons.u0
make_conj_rapp.u0 <= make_conj_app.u0 [private-mono,fragile,default]
File "./theories/micromega/Refl.v", line 138, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
not_make_conj_cons.u0 <= make_conj_cons.u0 [private-mono,fragile,default]
File "./theories/micromega/Refl.v", line 152, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
not_make_conj_app.u0 <= not_make_conj_cons.u0 [private-mono,fragile,default]
File "./theories/setoid_ring/Ring_theory.v", line 60, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.Ring_theory.1 <= Coq.Classes.Morphisms.51
[private-mono,fragile,default]
File "./theories/setoid_ring/Ring_theory.v", line 249, characters 34-38:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.Ring_theory.100 <= rewrite_relation_eq_dom.u0
Coq.setoid_ring.Ring_theory.100 <= rewrite_relation_eq_dom.u1
Coq.setoid_ring.Ring_theory.100 <= eq_rewrite_relation.u0
[private-mono,fragile,default]
File "./theories/setoid_ring/Ring_theory.v", line 354, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.Ring_theory.100 <= default_relation.u0
Coq.setoid_ring.Ring_theory.100 <= equivalence_default.u0
[private-mono,fragile,default]
File "./theories/Lists/ListSet.v", line 94, characters 38-42:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.ListSet.1 <= Coq.Lists.List.13 [private-mono,fragile,default]
File "./theories/Lists/ListSet.v", line 448, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.ListSet.1 <= set_mem_ind2.u0 [private-mono,fragile,default]
File "./theories/Lists/ListDec.v", line 121, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
uniquify_map.u0 <= Coq.Lists.ListDec.3 [private-mono,fragile,default]
File "./theories/Lists/ListDec.v", line 128, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
uniquify.u0 <= uniquify_map.u0
uniquify.u0 <= uniquify_map.u1
uniquify.u0 <= map_id.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 58, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
eq_nth_iff.u0 < eq.u0
eq_nth_iff.u0 <= rect2.u0
eq_nth_iff.u0 <= rect2.u1 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 62, characters 42-46:
Warning: Adding constraints to the global env from Qed body:
nth_order_hd.u0 <= eta.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 72, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
nth_order_tl.u0 <= eta.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 137, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
nth_order_replace_eq.u0 <= nth_replace_eq.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 148, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
nth_order_replace_neq.u0 <= nth_replace_neq.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 155, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
replace_id.u0 <= eta.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 163, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
replace_replace_eq.u0 <= eta.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 179, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
replace_replace_neq.u0 < eq.u0
replace_replace_neq.u0 <= rectS.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 233, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
map_ext_in.u1 < eq.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 239, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
map_ext.u0 <= map_ext_in.u0
map_ext.u1 <= map_ext_in.u1 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 247, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
nth_map.u0 <= caseS.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 289, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fold_left_right_assoc_eq.u0 < eq.u0
fold_left_right_assoc_eq.u1 < eq.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 356, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
append_splitat.u0 <= eta.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 364, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
append_inj.u0 <= pair_equal_spec.u0
append_inj.u0 <= pair_equal_spec.u1
append_inj.u0 <= splitat.u0
append_inj.u0 <= splitat_append.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 402, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Forall_forall.u0 <= sigT.u1
Forall_forall.u0 <= eq.u0
Forall_forall.u0 <= In_cons_iff.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 412, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Forall_cons_iff.u0 <= In.u0
Forall_cons_iff.u0 <= Forall_forall.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 420, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Forall_map.u0 <= Forall_cons_iff.u0
Forall_map.u1 <= Forall_cons_iff.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 452, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Forall_nth_order.u0 <= Forall_nth.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 466, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Forall2_nth.u0 <= rect2.u0
Forall2_nth.u0 <= rect2.u1 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 479, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Forall2_nth_order.u0 <= nth_order_ext.u0
Forall2_nth_order.u0 <= Forall2_nth.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 497, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
shiftin_nth.u0 <= caseS.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 512, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
shiftrepeat_nth.u0 <= nil_spec.u0
shiftrepeat_nth.u0 <= eta.u0
shiftrepeat_nth.u0 <= tl.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 541, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
In_shiftin.u0 <= In_cons_iff.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 549, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Forall_shiftin.u0 <= Forall_cons_iff.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 569, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
rev_cons.u0 <= rew_compose.u1 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 577, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
rev_shiftin.u0 <= rev_nil.u0
rev_shiftin.u0 <= rev_cons.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 584, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
rev_rev.u0 <= rev_nil.u0
rev_rev.u0 <= rev_cons.u0
rev_rev.u0 <= rev_shiftin.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 592, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
map_rev.u0 <= map_shiftin.u0
map_rev.u0 <= rev_nil.u0
map_rev.u0 <= rev_cons.u0
map_rev.u1 <= map_shiftin.u1
map_rev.u1 <= rev_nil.u0
map_rev.u1 <= rev_cons.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 600, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fold_left_rev_right.u0 <= fold_right_shiftin.u0
fold_left_rev_right.u0 <= rev_nil.u0
fold_left_rev_right.u0 <= rev_cons.u0
fold_left_rev_right.u1 <= fold_right_shiftin.u1
[private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 608, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
In_rev.u0 <= eq.u0
In_rev.u0 <= shiftin.u0
In_rev.u0 <= In_cons_iff.u0
In_rev.u0 <= In_shiftin.u0
In_rev.u0 <= rev_nil.u0
In_rev.u0 <= rev_cons.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 616, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Forall_rev.u0 <= shiftin.u0
Forall_rev.u0 <= Forall_cons_iff.u0
Forall_rev.u0 <= Forall_shiftin.u0
Forall_rev.u0 <= rev_nil.u0
Forall_rev.u0 <= rev_cons.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 625, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
to_list_of_list_opp.u0 < eq.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 640, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
of_list_to_list_opp.u0 < eq.u0
of_list_to_list_opp.u0 <= case0.u0
of_list_to_list_opp.u0 <= map_subst_map.u1
of_list_to_list_opp.u0 <= map_subst_map.u3 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 655, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
to_list_nil_iff.u0 <= case0.u0
to_list_nil_iff.u0 <= to_list_nil.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 664, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
to_list_inj.u0 <= eta.u0
to_list_inj.u0 <= caseS.u2
to_list_inj.u0 <= hd.u0
to_list_inj.u0 <= tl.u0
to_list_inj.u0 <= to_list_nil_iff.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 668, characters 28-32:
Warning: Adding constraints to the global env from Qed body:
to_list_hd.u0 <= eta.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 678, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
to_list_last.u0 <= eta.u0
to_list_last.u0 <= to_list_cons.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 698, characters 28-32:
Warning: Adding constraints to the global env from Qed body:
to_list_tl.u0 <= eta.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 705, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
to_list_append.u0 < eq.u0
to_list_append.u0 <= to_list_cons.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 713, characters 93-97:
Warning: Adding constraints to the global env from Qed body:
to_list_rev_append.u0 <= to_list_rev_append_tail.u0
[private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 720, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
to_list_rev.u0 <= to_list_rev_append.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 735, characters 56-60:
Warning: Adding constraints to the global env from Qed body:
to_list_fold_right.u1 <= eq.u0 [private-mono,fragile,default]
File "./theories/Vectors/VectorSpec.v", line 778, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
to_list_Forall2.u1 <= case0.u0
to_list_Forall2.u1 <= eta.u0
to_list_Forall2.u1 <= hd.u0
to_list_Forall2.u1 <= tl.u0 [private-mono,fragile,default]
File "./theories/Logic/FinFun.v", line 48, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Listing_decidable_eq.u0 <= Coq.Lists.ListDec.3 [private-mono,fragile,default]
File "./theories/Logic/FinFun.v", line 61, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Finite_dec.u0 <= uniquify.u0
Finite_dec.u0 <= Listing_decidable_eq.u0 [private-mono,fragile,default]
File "./theories/Logic/FinFun.v", line 69, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Finite_alt_deprecated.u0 <= Finite_dec.u0 [private-mono,fragile,default]
File "./theories/Logic/FinFun.v", line 93, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Injective_list_carac.u0 <= Injective_map_NoDup.u0
Injective_list_carac.u1 <= Injective_map_NoDup.u1
[private-mono,fragile,default]
File "./theories/Logic/FinFun.v", line 112, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Injective_carac.u0 <= Injective_map_NoDup.u0
Injective_carac.u1 <= Injective_map_NoDup.u1 [private-mono,fragile,default]
File "./theories/Logic/FinFun.v", line 146, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Surjective_carac.u0 <= uniquify_map.u0
Surjective_carac.u0 <= Surjective_list_carac.u1
Surjective_carac.u1 <= uniquify_map.u1
Surjective_carac.u1 <= Surjective_list_carac.u0
[private-mono,fragile,default]
File "./theories/Logic/FinFun.v", line 174, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Endo_Injective_Surjective.u0 <= Listing.u0
Endo_Injective_Surjective.u0 <= Finite'.u0
Endo_Injective_Surjective.u0 <= Finite_dec.u0
Endo_Injective_Surjective.u0 <= Injective_carac.u0
Endo_Injective_Surjective.u0 <= Injective_carac.u1
Endo_Injective_Surjective.u0 <= Surjective_carac.u0
Endo_Injective_Surjective.u0 <= Surjective_carac.u1
Endo_Injective_Surjective.u0 <= Coq.Lists.List.314
Endo_Injective_Surjective.u0 <= Coq.Lists.List.315
Endo_Injective_Surjective.u0 <= Coq.Lists.List.524
Endo_Injective_Surjective.u0 <= Coq.Lists.List.677
Endo_Injective_Surjective.u0 <= NoDup_map_inv.u0
Endo_Injective_Surjective.u0 <= NoDup_map_inv.u1
[private-mono,fragile,default]
File "./theories/Logic/FinFun.v", line 221, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Surjective_inverse.u0 <= Coq.Init.Logic.2
Surjective_inverse.u0 <= Finite_Empty_or_not.u0
Surjective_inverse.u0 <= Coq.Lists.List.437 [private-mono,fragile,default]
File "./theories/Logic/FinFun.v", line 233, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Injective_Surjective_Bijective.u0 <= Surjective_inverse.u0
Injective_Surjective_Bijective.u1 <= Surjective_inverse.u1
[private-mono,fragile,default]
File "./theories/Vectors/VectorEq.v", line 59, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
Coq.Vectors.VectorEq.1 < eq.u0
Coq.Vectors.VectorEq.1 <= cons_inj.u0
Coq.Vectors.VectorEq.1 <= rect2.u0
Coq.Vectors.VectorEq.1 <= rect2.u1 [private-mono,fragile,default]
File "./theories/Lists/SetoidList.v", line 850, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.SetoidList.1 <= default_relation.u0
Coq.Lists.SetoidList.1 <= equivalence_default.u0
[private-mono,fragile,default]
File "./theories/Sorting/Permutation.v", line 107, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Permutation_morph_transp.u0 <= Coq.Lists.List.13
[private-mono,fragile,default]
File "./theories/Sorting/Permutation.v", line 150, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.Permutation.32 <= Coq.Lists.List.13
[private-mono,fragile,default]
File "./theories/Sorting/Permutation.v", line 179, characters 63-67:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.Permutation.32 <= Permutation_Equivalence.u0
Coq.Sorting.Permutation.32 <= Permutation_cons.u0
Coq.Sorting.Permutation.32 <= Coq.Classes.Morphisms.51
[private-mono,fragile,default]
File "./theories/Sorting/Permutation.v", line 592, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.Permutation.32 <= Forall2_flip.u0
Coq.Sorting.Permutation.32 <= Forall2_flip.u1 [private-mono,fragile,default]
File "./theories/Sorting/Permutation.v", line 658, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.Permutation.60 <= Permutation_Equivalence.u0
Coq.Sorting.Permutation.60 <= Coq.Sorting.Permutation.32
[private-mono,fragile,default]
File "./theories/Sorting/Permutation.v", line 800, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.Permutation.87 <= Permutation_Equivalence.u0
Coq.Sorting.Permutation.87 <= Coq.Sorting.Permutation.32
[private-mono,fragile,default]
File "./theories/Sorting/Permutation.v", line 927, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.Permutation.115 <= Coq.Lists.List.13
[private-mono,fragile,default]
File "./theories/Sorting/Permutation.v", line 942, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.Permutation.115 <= Permutation_Equivalence.u0
Coq.Sorting.Permutation.115 <= Coq.Sorting.Permutation.32
[private-mono,fragile,default]
File "./theories/Structures/OrderedType.v", line 114, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= proper_sym_impl_iff_2.u1 [private-mono,fragile,default]
File "./theories/Sorting/Mergesort.v", line 162, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= Coq.Sorting.Permutation.32 [private-mono,fragile,default]
File "./theories/Lists/SetoidPermutation.v", line 67, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.SetoidPermutation.1 <= Coq.Lists.List.13
[private-mono,fragile,default]
File "./theories/Lists/SetoidPermutation.v", line 73, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.SetoidPermutation.1 <= Coq.Classes.Morphisms.51
[private-mono,fragile,default]
File "./theories/Lists/SetoidPermutation.v", line 165, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Lists.SetoidPermutation.1 <= Permutation_Equivalence.u0
[private-mono,fragile,default]
File "./theories/Sorting/CPermutation.v", line 36, characters 53-57:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.CPermutation.1 <= Coq.Sorting.Permutation.32
[private-mono,fragile,default]
File "./theories/Sorting/CPermutation.v", line 127, characters 56-60:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.CPermutation.26 <= CPermutation_Equivalence.u0
[private-mono,fragile,default]
File "./theories/Sorting/CPermutation.v", line 216, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
CPermutation_rev.u0 <= CPermutation_Equivalence.u0
CPermutation_rev.u0 <= Coq.Sorting.CPermutation.26
[private-mono,fragile,default]
File "./theories/Sorting/CPermutation.v", line 227, characters 65-69:
Warning: Adding constraints to the global env from Qed body:
CPermutation_in'.u0 <= CPermutation_Equivalence.u0
CPermutation_in'.u0 <= CPermutation_in.u0 [private-mono,fragile,default]
File "./theories/Sorting/CPermutation.v", line 247, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
CPermutation_map_inv.u1 <= CPermutation_Equivalence.u0
CPermutation_map_inv.u1 <= Coq.Sorting.CPermutation.26
[private-mono,fragile,default]
File "./theories/Sorting/CPermutation.v", line 254, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
CPermutation_image.u0 <= Coq.Sorting.Permutation.60
CPermutation_image.u1 <= Coq.Sorting.Permutation.60
[private-mono,fragile,default]
File "./theories/Sorting/CPermutation.v", line 288, characters 57-61:
Warning: Adding constraints to the global env from Qed body:
CPermutation_rewrite_rev.u0 <= CPermutation_Equivalence.u0
CPermutation_rewrite_rev.u0 <= CPermutation_rev.u0
CPermutation_rewrite_rev.u0 <= Coq.Classes.Morphisms.95
CPermutation_rewrite_rev.u0 <= flip_arrow.u0
CPermutation_rewrite_rev.u0 <= flip_arrow.u1 [private-mono,fragile,default]
File "./theories/Structures/OrdersAlt.v", line 173, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= proper_sym_impl_iff_2.u1 [private-mono,fragile,default]
File "./theories/Structures/EqualitiesFacts.v", line 90, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
InA_eqk.u0 <= eqk_equiv.u0 [private-mono,fragile,default]
File "./theories/Structures/EqualitiesFacts.v", line 108, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
In_alt.u0 <= eqke_equiv.u0
In_alt.u0 <= Coq.Classes.RelationPairs.30
In_alt.u0 <= InA_eqke_eqk.u0
In_alt.u0 <= InA_eqk_eqke.u0 [private-mono,fragile,default]
File "./theories/Structures/EqualitiesFacts.v", line 114, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
In_alt'.u0 <= InA_eqk.u0
In_alt'.u0 <= In_alt.u0 [private-mono,fragile,default]
File "./theories/Structures/EqualitiesFacts.v", line 123, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
In_alt2.u0 <= Morphisms_Prop.ex_iff_morphism_obligation_1.u0
[private-mono,fragile,default]
File "./theories/Structures/EqualitiesFacts.v", line 128, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
In_nil.u0 <= In_alt2.u0 [private-mono,fragile,default]
File "./theories/Structures/EqualitiesFacts.v", line 134, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
In_cons.u0 <= In_alt2.u0 [private-mono,fragile,default]
File "./theories/Structures/EqualitiesFacts.v", line 142, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
MapsTo_compat.u0 <= eqke_equiv.u0
MapsTo_compat.u0 <= Coq.Classes.RelationPairs.30
[private-mono,fragile,default]
File "./theories/Structures/EqualitiesFacts.v", line 149, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
In_compat.u0 <= Morphisms_Prop.ex_iff_morphism_obligation_1.u0
In_compat.u0 <= eqk_equiv.u0
In_compat.u0 <= eqke_eqk.u0
In_compat.u0 <= Coq.Classes.RelationPairs.30
In_compat.u0 <= In_alt.u0 [private-mono,fragile,default]
File "./theories/Structures/EqualitiesFacts.v", line 153, characters 23-27:
Warning: Adding constraints to the global env from Qed body:
MapsTo_eq.u0 <= eqke_equiv.u0
MapsTo_eq.u0 <= MapsTo_compat.u0 [private-mono,fragile,default]
File "./theories/Structures/EqualitiesFacts.v", line 157, characters 23-27:
Warning: Adding constraints to the global env from Qed body:
In_eq.u0 <= eqk.u0
In_eq.u0 <= eqk_equiv.u0
In_eq.u0 <= In_compat.u0 [private-mono,fragile,default]
File "./theories/Structures/EqualitiesFacts.v", line 164, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
In_inv.u0 <= eqke_def.u0 [private-mono,fragile,default]
File "./theories/Structures/EqualitiesFacts.v", line 170, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
In_inv_2.u0 <= eqk_def.u0 [private-mono,fragile,default]
File "./theories/Structures/EqualitiesFacts.v", line 177, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
In_inv_3.u0 <= eqke_1.u0 [private-mono,fragile,default]
File "./theories/ZArith/Zmisc.v", line 31, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iter_nat_of_Z.u0 <= Pos2Nat.inj_iter.u0 [private-mono,fragile,default]
File "./theories/Structures/OrdersLists.v", line 81, characters 38-42:
Warning: Adding constraints to the global env from Qed body:
ltk_compat.u0 <= Coq.Classes.RelationPairs.29 [private-mono,fragile,default]
File "./theories/Structures/OrdersLists.v", line 85, characters 49-53:
Warning: Adding constraints to the global env from Qed body:
ltk_compat'.u0 <= eqke_eqk.u0
ltk_compat'.u0 <= ltk_compat.u0 [private-mono,fragile,default]
File "./theories/Structures/OrdersLists.v", line 91, characters 27-31:
Warning: Adding constraints to the global env from Qed body:
pair_compat.u0 <= Coq.Classes.RelationPairs.30 [private-mono,fragile,default]
File "./theories/Structures/OrdersLists.v", line 102, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Structures.OrdersLists.46 <= eqk_equiv.u0
Coq.Structures.OrdersLists.46 <= Coq.Classes.RelationPairs.29
Coq.Structures.OrdersLists.46 <= ltk_strorder.u0
[private-mono,fragile,default]
File "./theories/Structures/OrdersLists.v", line 108, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Structures.OrdersLists.46 <= eqke_equiv.u0
Coq.Structures.OrdersLists.46 <= ltk_compat'.u0
[private-mono,fragile,default]
File "./theories/Structures/OrdersLists.v", line 114, characters 24-28:
Warning: Adding constraints to the global env from Qed body:
Coq.Structures.OrdersLists.46 <= Coq.Lists.SetoidList.1
[private-mono,fragile,default]
File "./theories/Structures/OrdersLists.v", line 134, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Structures.OrdersLists.46 <= InA_eqke_eqk.u0
[private-mono,fragile,default]
File "./theories/Structures/OrdersLists.v", line 156, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Structures.OrdersLists.46 <= In_eq.u0 [private-mono,fragile,default]
File "./theories/MSets/MSetInterface.v", line 539, characters 33-37:
Warning: Adding constraints to the global env from Qed body:
M.fold_spec.u0 = fold_spec.u0 [private-mono,fragile,default]
File "./theories/MSets/MSetInterface.v", line 727, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= Coq.Classes.Morphisms.51 [private-mono,fragile,default]
File "./theories/ZArith/Wf_Z.v", line 116, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
natlike_rec2.u0 <= well_founded_induction_type.u0
natlike_rec2.u0 <= eq_rect_r.u0 [private-mono,fragile,default]
File "./theories/ZArith/Wf_Z.v", line 136, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
natlike_rec3.u0 <= well_founded_induction_type.u0
[private-mono,fragile,default]
File "./theories/ZArith/Wf_Z.v", line 170, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Z_lt_rec.u0 <= Zlt_0_rec.u0 [private-mono,fragile,default]
File "./theories/ZArith/Wf_Z.v", line 197, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Zlt_lower_bound_rec.u0 <= Zlt_0_rec.u0
Zlt_lower_bound_rec.u0 <= Coq.Init.Logic.10 [private-mono,fragile,default]
File "./theories/FSets/FSetBridge.v", line 121, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold.u0 <= M.fold.u0
fold.u0 <= fold_1.u0 [private-mono,fragile,default]
File "./theories/micromega/Tauto.v", line 288, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
rtyp.u0 <= Coq.Classes.Morphisms.51 [private-mono,fragile,default]
File "./theories/micromega/Tauto.v", line 881, characters 6-10:
Warning: Adding constraints to the global env from Qed body:
Coq.micromega.Tauto.51 <= if_same.u0
Coq.micromega.Tauto.52 <= if_same.u0 [private-mono,fragile,default]
File "./theories/micromega/Tauto.v", line 1036, characters 6-10:
Warning: Adding constraints to the global env from Qed body:
Coq.micromega.Tauto.148 <= is_bool_inv.u0
Coq.micromega.Tauto.149 <= is_bool_inv.u1 [private-mono,fragile,default]
File "./theories/micromega/Tauto.v", line 1451, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
rxcnf_xcnf.u0 <= Coq.micromega.Tauto.148
rxcnf_xcnf.u0 <= rxcnf_and_xcnf.u0
rxcnf_xcnf.u0 <= rxcnf_or_xcnf.u0
rxcnf_xcnf.u0 <= rxcnf_impl_xcnf.u0
rxcnf_xcnf.u0 <= rxcnf_iff_xcnf.u0
rxcnf_xcnf.u1 <= Coq.micromega.Tauto.149
rxcnf_xcnf.u1 <= rxcnf_and_xcnf.u1
rxcnf_xcnf.u1 <= rxcnf_or_xcnf.u1
rxcnf_xcnf.u1 <= rxcnf_impl_xcnf.u1
rxcnf_xcnf.u1 <= rxcnf_iff_xcnf.u1 [private-mono,fragile,default]
File "./theories/micromega/Tauto.v", line 1478, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.micromega.Tauto.51 <= make_conj_app.u0
Coq.micromega.Tauto.51 <= make_conj_rapp.u0
Coq.micromega.Tauto.52 <= make_conj_app.u0
Coq.micromega.Tauto.52 <= make_conj_rapp.u0 [private-mono,fragile,default]
File "./theories/micromega/Tauto.v", line 1890, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
rtyp.u0 <= Coq.micromega.Tauto.148 [private-mono,fragile,default]
File "./theories/micromega/Tauto.v", line 2053, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.micromega.Tauto.51 <= make_conj_impl.u0
Coq.micromega.Tauto.52 <= make_conj_impl.u0 [private-mono,fragile,default]
File "./theories/Numbers/Natural/Abstract/NDefOps.v", line 38, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
if_zero_wd.u0 <= recursion_wd.u0 [private-mono,fragile,default]
File "./theories/Numbers/Natural/Abstract/NDefOps.v", line 43, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
if_zero_0.u0 <= recursion_0.u0 [private-mono,fragile,default]
File "./theories/Numbers/Natural/Abstract/NDefOps.v", line 50, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
if_zero_succ.u0 <= Coq.Classes.Morphisms.1
if_zero_succ.u0 <= Coq.Classes.RelationClasses.1
if_zero_succ.u0 <= recursion_succ.u0
if_zero_succ.u0 <= Coq.Classes.Morphisms.51 [private-mono,fragile,default]
File "./theories/Numbers/Natural/Abstract/NDefOps.v", line 144, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= equivalence_rewrite_relation.u0 [private-mono,fragile,default]
File "./theories/Numbers/Natural/Abstract/NDefOps.v", line 221, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= Coq.Classes.RelationPairs.29
t.u0 <= Coq.Classes.RelationPairs.30 [private-mono,fragile,default]
File "./theories/FSets/FMapWeakList.v", line 649, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapWeakList.132 <= Coq.FSets.FMapWeakList.129
[private-mono,fragile,default]
File "./theories/FSets/FMapWeakList.v", line 968, characters 52-56:
Warning: Adding constraints to the global env from Qed body:
Raw.fold_1.u0 = fold_1.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapList.v", line 743, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= eq.u0
Coq.FSets.FMapList.105 <= Coq.FSets.FMapList.103
[private-mono,fragile,default]
File "./theories/FSets/FMapList.v", line 1077, characters 52-56:
Warning: Adding constraints to the global env from Qed body:
Raw.fold_1.u0 = fold_1.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapList.v", line 1297, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Raw.t.u0 <= Coq.Init.Datatypes.51 [private-mono,fragile,default]
File "./theories/setoid_ring/Ncring.v", line 135, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.Ncring.274 <= Coq.Classes.Morphisms.51
[private-mono,fragile,default]
File "./theories/setoid_ring/Ncring.v", line 189, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
Zero.u0 <= zero_notation.u0
Coq.setoid_ring.Ncring.274 <= default_relation.u0
Coq.setoid_ring.Ncring.274 <= equivalence_default.u0
[private-mono,fragile,default]
File "./theories/setoid_ring/Ring_polynom.v", line 74, characters 42-46:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.Ring_polynom.1 <= Coq.setoid_ring.Ring_theory.100
[private-mono,fragile,default]
File "./theories/setoid_ring/Ring_polynom.v", line 531, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.Ring_polynom.2 <= Coq.Classes.Morphisms.51
[private-mono,fragile,default]
File "./theories/setoid_ring/Ring_polynom.v", line 594, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.Ring_polynom.1 <= Seq_refl.u0 [private-mono,fragile,default]
File "./theories/micromega/EnvRing.v", line 124, characters 42-46:
Warning: Adding constraints to the global env from Qed body:
Coq.micromega.EnvRing.9 <= Coq.setoid_ring.Ring_theory.100
[private-mono,fragile,default]
File "./theories/micromega/EnvRing.v", line 598, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.micromega.EnvRing.9 < eq.u0 [private-mono,fragile,default]
File "./theories/micromega/EnvRing.v", line 624, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
Coq.micromega.EnvRing.9 <= Seq_refl.u0 [private-mono,fragile,default]
File "./theories/setoid_ring/InitialRing.v", line 123, characters 44-48:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.InitialRing.1 <= Coq.setoid_ring.Ring_theory.100
[private-mono,fragile,default]
File "./theories/setoid_ring/InitialRing.v", line 133, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.InitialRing.1 <= Seq_refl.u0 [private-mono,fragile,default]
File "./theories/setoid_ring/InitialRing.v", line 429, characters 44-48:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.InitialRing.49 <= Coq.setoid_ring.Ring_theory.100
[private-mono,fragile,default]
File "./theories/setoid_ring/InitialRing.v", line 615, characters 43-47:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.InitialRing.70 <= Coq.setoid_ring.Ring_theory.100
[private-mono,fragile,default]
File "./theories/setoid_ring/InitialRing.v", line 641, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.InitialRing.70 <= Seq_refl.u0 [private-mono,fragile,default]
File "./theories/micromega/OrderedRing.v", line 137, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
hypo.u0 < list.u0 [private-mono,fragile,default]
File "./theories/QArith/QArith_base.v", line 463, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
hypo.u0 < list.u0 [private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 442, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fun_choice_iff_rel_choice_and_functional_rel_reification.u0 <= functional_rel_reification_and_rel_choice_imp_fun_choice.u0
fun_choice_iff_rel_choice_and_functional_rel_reification.u0 <= fun_choice_imp_rel_choice.u0
fun_choice_iff_rel_choice_and_functional_rel_reification.u0 <= fun_choice_imp_functional_rel_reification.u0
fun_choice_iff_rel_choice_and_functional_rel_reification.u1 <= functional_rel_reification_and_rel_choice_imp_fun_choice.u1
fun_choice_iff_rel_choice_and_functional_rel_reification.u1 <= fun_choice_imp_rel_choice.u1
fun_choice_iff_rel_choice_and_functional_rel_reification.u1 <= fun_choice_imp_functional_rel_reification.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 476, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
rel_choice_and_proof_irrel_imp_guarded_rel_choice.u2 <= sigT.u0
rel_choice_and_proof_irrel_imp_guarded_rel_choice.u2 <= Coq.Init.Specif.22
rel_choice_and_proof_irrel_imp_guarded_rel_choice.u2 <= rel_choice_and_proof_irrel_imp_guarded_rel_choice.u0
rel_choice_and_proof_irrel_imp_guarded_rel_choice.u3 <= rel_choice_and_proof_irrel_imp_guarded_rel_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 490, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
rel_choice_indep_of_general_premises_imp_guarded_rel_choice.u1 <= IndependenceOfGeneralPremises.u0
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 507, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
subset_types_imp_guarded_rel_choice_iff_rel_choice.u0 <= rel_choice_and_proof_irrel_imp_guarded_rel_choice.u2
subset_types_imp_guarded_rel_choice_iff_rel_choice.u1 <= rel_choice_and_proof_irrel_imp_guarded_rel_choice.u3
subset_types_imp_guarded_rel_choice_iff_rel_choice.u2 <= guarded_rel_choice_imp_rel_choice.u0
subset_types_imp_guarded_rel_choice_iff_rel_choice.u2 <= subset_types_imp_guarded_rel_choice_iff_rel_choice.u0
subset_types_imp_guarded_rel_choice_iff_rel_choice.u3 <= guarded_rel_choice_imp_rel_choice.u1
subset_types_imp_guarded_rel_choice_iff_rel_choice.u3 <= subset_types_imp_guarded_rel_choice_iff_rel_choice.u1
rel_choice_and_proof_irrel_imp_guarded_rel_choice.u0 = subset_types_imp_guarded_rel_choice_iff_rel_choice.u2
rel_choice_and_proof_irrel_imp_guarded_rel_choice.u1 = subset_types_imp_guarded_rel_choice_iff_rel_choice.u3
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 519, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
guarded_iff_omniscient_rel_choice.u0 = guarded_iff_omniscient_rel_choice.u2
guarded_iff_omniscient_rel_choice.u1 = guarded_iff_omniscient_rel_choice.u3
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 533, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
IndependenceOfGeneralPremises.u0 <= guarded_fun_choice_imp_indep_of_general_premises.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 543, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
guarded_fun_choice_imp_fun_choice.u2 <= guarded_fun_choice_imp_fun_choice.u0
guarded_fun_choice_imp_fun_choice.u3 <= guarded_fun_choice_imp_fun_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 552, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fun_choice_and_indep_general_prem_imp_guarded_fun_choice.u2 <= fun_choice_and_indep_general_prem_imp_guarded_fun_choice.u0
fun_choice_and_indep_general_prem_imp_guarded_fun_choice.u3 <= IndependenceOfGeneralPremises.u0
fun_choice_and_indep_general_prem_imp_guarded_fun_choice.u3 <= fun_choice_and_indep_general_prem_imp_guarded_fun_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 562, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fun_choice_and_indep_general_prem_iff_guarded_fun_choice.u0 <= guarded_fun_choice_imp_fun_choice.u2
fun_choice_and_indep_general_prem_iff_guarded_fun_choice.u1 <= guarded_fun_choice_imp_fun_choice.u3
fun_choice_and_indep_general_prem_iff_guarded_fun_choice.u2 <= fun_choice_and_indep_general_prem_imp_guarded_fun_choice.u2
fun_choice_and_indep_general_prem_iff_guarded_fun_choice.u3 <= fun_choice_and_indep_general_prem_imp_guarded_fun_choice.u3
guarded_fun_choice_imp_indep_of_general_premises.u0 = guarded_fun_choice_imp_fun_choice.u0
guarded_fun_choice_imp_indep_of_general_premises.u0 = fun_choice_and_indep_general_prem_iff_guarded_fun_choice.u2
guarded_fun_choice_imp_indep_of_general_premises.u1 = guarded_fun_choice_imp_fun_choice.u1
guarded_fun_choice_imp_indep_of_general_premises.u1 = fun_choice_and_indep_general_prem_iff_guarded_fun_choice.u3
fun_choice_and_indep_general_prem_imp_guarded_fun_choice.u0 = fun_choice_and_indep_general_prem_iff_guarded_fun_choice.u0
fun_choice_and_indep_general_prem_imp_guarded_fun_choice.u1 = fun_choice_and_indep_general_prem_iff_guarded_fun_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 575, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
SmallDrinker'sParadox.u0 <= omniscient_fun_choice_imp_small_drinker.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 583, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
omniscient_fun_choice_imp_fun_choice.u2 <= omniscient_fun_choice_imp_fun_choice.u0
omniscient_fun_choice_imp_fun_choice.u3 <= omniscient_fun_choice_imp_fun_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 593, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fun_choice_and_small_drinker_imp_omniscient_fun_choice.u2 <= fun_choice_and_small_drinker_imp_omniscient_fun_choice.u0
fun_choice_and_small_drinker_imp_omniscient_fun_choice.u3 <= SmallDrinker'sParadox.u0
fun_choice_and_small_drinker_imp_omniscient_fun_choice.u3 <= fun_choice_and_small_drinker_imp_omniscient_fun_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 603, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fun_choice_and_small_drinker_iff_omniscient_fun_choice.u0 <= omniscient_fun_choice_imp_fun_choice.u2
fun_choice_and_small_drinker_iff_omniscient_fun_choice.u1 <= omniscient_fun_choice_imp_fun_choice.u3
fun_choice_and_small_drinker_iff_omniscient_fun_choice.u2 <= fun_choice_and_small_drinker_imp_omniscient_fun_choice.u2
fun_choice_and_small_drinker_iff_omniscient_fun_choice.u3 <= fun_choice_and_small_drinker_imp_omniscient_fun_choice.u3
omniscient_fun_choice_imp_small_drinker.u0 = omniscient_fun_choice_imp_fun_choice.u0
omniscient_fun_choice_imp_small_drinker.u0 = fun_choice_and_small_drinker_iff_omniscient_fun_choice.u2
omniscient_fun_choice_imp_small_drinker.u1 = omniscient_fun_choice_imp_fun_choice.u1
omniscient_fun_choice_imp_small_drinker.u1 = fun_choice_and_small_drinker_iff_omniscient_fun_choice.u3
fun_choice_and_small_drinker_imp_omniscient_fun_choice.u0 = fun_choice_and_small_drinker_iff_omniscient_fun_choice.u0
fun_choice_and_small_drinker_imp_omniscient_fun_choice.u1 = fun_choice_and_small_drinker_iff_omniscient_fun_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 619, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
guarded_iff_omniscient_fun_choice.u0 = guarded_iff_omniscient_fun_choice.u2
guarded_iff_omniscient_fun_choice.u1 = guarded_iff_omniscient_fun_choice.u3
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 633, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iota_imp_constructive_definite_description.u1 <= iota_imp_constructive_definite_description.u0
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 644, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
epsilon_imp_constructive_indefinite_description.u1 <= epsilon_imp_constructive_indefinite_description.u0
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 652, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
constructive_indefinite_description_and_small_drinker_imp_epsilon.u1 <= SmallDrinker'sParadox.u0
constructive_indefinite_description_and_small_drinker_imp_epsilon.u1 <= constructive_indefinite_description_and_small_drinker_imp_epsilon.u0
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 658, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
SmallDrinker'sParadox.u0 <= epsilon_imp_small_drinker.u0
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 670, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
constructive_indefinite_description_and_small_drinker_iff_epsilon.u1 < Coq.Init.Datatypes.23
Coq.Logic.ChoiceFacts.1 <= Coq.Init.Datatypes.23
constructive_indefinite_description_and_small_drinker_iff_epsilon.u1 <= constructive_indefinite_description_and_small_drinker_imp_epsilon.u1
constructive_indefinite_description_and_small_drinker_iff_epsilon.u3 <= epsilon_imp_constructive_indefinite_description.u1
epsilon_imp_constructive_indefinite_description.u0 = epsilon_imp_small_drinker.u0
epsilon_imp_constructive_indefinite_description.u0 = constructive_indefinite_description_and_small_drinker_iff_epsilon.u2
constructive_indefinite_description_and_small_drinker_imp_epsilon.u0 = constructive_indefinite_description_and_small_drinker_iff_epsilon.u0
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 721, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
dep_non_dep_functional_choice.u2 <= dep_non_dep_functional_choice.u0
dep_non_dep_functional_choice.u3 <= dep_non_dep_functional_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 747, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
non_dep_dep_functional_choice.u2 <= sigT.u0
non_dep_dep_functional_choice.u2 <= eq.u0
non_dep_dep_functional_choice.u2 <= Coq.Init.Specif.22
non_dep_dep_functional_choice.u2 <= non_dep_dep_functional_choice.u0
non_dep_dep_functional_choice.u2 <= non_dep_dep_functional_choice.u1
non_dep_dep_functional_choice.u3 <= sigT.u1
non_dep_dep_functional_choice.u3 <= Coq.Init.Logic.10
non_dep_dep_functional_choice.u3 <= Coq.Init.Specif.23
non_dep_dep_functional_choice.u3 <= non_dep_dep_functional_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 763, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
functional_choice_to_inhabited_forall_commute.u2 <= ex.u0
functional_choice_to_inhabited_forall_commute.u2 <= non_dep_dep_functional_choice.u2
functional_choice_to_inhabited_forall_commute.u3 <= sig.u0
functional_choice_to_inhabited_forall_commute.u3 <= ex.u0
functional_choice_to_inhabited_forall_commute.u3 <= inhabited_sig_to_exists.u0
functional_choice_to_inhabited_forall_commute.u3 <= non_dep_dep_functional_choice.u3
functional_choice_to_inhabited_forall_commute.u3 <= inhabited_covariant.u0
functional_choice_to_inhabited_forall_commute.u3 <= inhabited_covariant.u1
non_dep_dep_functional_choice.u0 = functional_choice_to_inhabited_forall_commute.u0
non_dep_dep_functional_choice.u1 = functional_choice_to_inhabited_forall_commute.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 774, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
inhabited_forall_commute_to_functional_choice.u2 <= inhabited_forall_commute_to_functional_choice.u0
inhabited_forall_commute_to_functional_choice.u3 <= Coq.Init.Specif.16
inhabited_forall_commute_to_functional_choice.u3 <= exists_to_inhabited_sig.u0
inhabited_forall_commute_to_functional_choice.u3 <= inhabited_forall_commute_to_functional_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 786, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
dep_non_dep_functional_rel_reification.u2 <= dep_non_dep_functional_rel_reification.u0
dep_non_dep_functional_rel_reification.u3 <= dep_non_dep_functional_rel_reification.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 810, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
non_dep_dep_functional_rel_reification.u2 <= sigT.u0
non_dep_dep_functional_rel_reification.u2 <= eq.u0
non_dep_dep_functional_rel_reification.u2 <= Coq.Init.Specif.22
non_dep_dep_functional_rel_reification.u2 <= non_dep_dep_functional_rel_reification.u0
non_dep_dep_functional_rel_reification.u2 <= non_dep_dep_functional_rel_reification.u1
non_dep_dep_functional_rel_reification.u3 <= sigT.u1
non_dep_dep_functional_rel_reification.u3 <= Coq.Init.Logic.10
non_dep_dep_functional_rel_reification.u3 <= Coq.Init.Specif.23
non_dep_dep_functional_rel_reification.u3 <= non_dep_dep_functional_rel_reification.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 818, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
dep_iff_non_dep_functional_rel_reification.u0 <= dep_non_dep_functional_rel_reification.u2
dep_iff_non_dep_functional_rel_reification.u1 <= dep_non_dep_functional_rel_reification.u3
dep_iff_non_dep_functional_rel_reification.u2 <= non_dep_dep_functional_rel_reification.u2
dep_iff_non_dep_functional_rel_reification.u3 <= non_dep_dep_functional_rel_reification.u3
dep_non_dep_functional_rel_reification.u0 = dep_iff_non_dep_functional_rel_reification.u2
dep_non_dep_functional_rel_reification.u1 = dep_iff_non_dep_functional_rel_reification.u3
non_dep_dep_functional_rel_reification.u0 = dep_iff_non_dep_functional_rel_reification.u0
non_dep_dep_functional_rel_reification.u1 = dep_iff_non_dep_functional_rel_reification.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 841, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
relative_non_contradiction_of_indefinite_descr.u0 < ex.u0
relative_non_contradiction_of_indefinite_descr.u0 < sigT.u0
relative_non_contradiction_of_indefinite_descr.u0 < Coq.Init.Specif.22
relative_non_contradiction_of_indefinite_descr.u0 < non_dep_dep_functional_choice.u2
relative_non_contradiction_of_indefinite_descr.u0 <= sigT.u1
relative_non_contradiction_of_indefinite_descr.u0 <= Coq.Init.Specif.23
relative_non_contradiction_of_indefinite_descr.u0 <= non_dep_dep_functional_choice.u3
relative_non_contradiction_of_indefinite_descr.u1 = non_dep_dep_functional_choice.u0
relative_non_contradiction_of_indefinite_descr.u2 = non_dep_dep_functional_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 850, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
constructive_indefinite_descr_fun_choice.u2 <= Coq.Init.Specif.16
constructive_indefinite_descr_fun_choice.u2 <= constructive_indefinite_descr_fun_choice.u0
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 870, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
relative_non_contradiction_of_definite_descr.u0 < ex.u0
relative_non_contradiction_of_definite_descr.u0 < sigT.u0
relative_non_contradiction_of_definite_descr.u0 < Coq.Init.Specif.22
relative_non_contradiction_of_definite_descr.u0 < non_dep_dep_functional_rel_reification.u2
relative_non_contradiction_of_definite_descr.u0 <= sigT.u1
relative_non_contradiction_of_definite_descr.u0 <= Coq.Init.Specif.23
relative_non_contradiction_of_definite_descr.u0 <= non_dep_dep_functional_rel_reification.u3
relative_non_contradiction_of_definite_descr.u1 = non_dep_dep_functional_rel_reification.u0
relative_non_contradiction_of_definite_descr.u2 = non_dep_dep_functional_rel_reification.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 879, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
constructive_definite_descr_fun_reification.u2 <= Coq.Init.Specif.16
constructive_definite_descr_fun_reification.u2 <= constructive_definite_descr_fun_reification.u0
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 944, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
relative_non_contradiction_of_definite_descr.u0 = constructive_definite_descr_excluded_middle.u0
relative_non_contradiction_of_definite_descr.u1 = fun_reification_descr_computational_excluded_middle_in_prop_context.u0
relative_non_contradiction_of_definite_descr.u2 = fun_reification_descr_computational_excluded_middle_in_prop_context.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 959, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
functional_choice_imp_functional_dependent_choice.u2 <= functional_choice_imp_functional_dependent_choice.u0
functional_choice_imp_functional_dependent_choice.u2 <= functional_choice_imp_functional_dependent_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 980, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
functional_dependent_choice_imp_functional_countable_choice.u1 <= functional_dependent_choice_imp_functional_countable_choice.u0
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 1006, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
repr_fun_choice_imp_ext_pred_repr.u1 <= Coq.Classes.RelationClasses.1
repr_fun_choice_imp_ext_pred_repr.u1 <= repr_fun_choice_imp_ext_pred_repr.u0
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 1016, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
repr_fun_choice_imp_ext_function_repr.u1 <= Coq.Classes.RelationClasses.1
repr_fun_choice_imp_ext_function_repr.u1 <= repr_fun_choice_imp_ext_function_repr.u0
repr_fun_choice_imp_ext_function_repr.u2 <= Coq.Classes.RelationClasses.1
repr_fun_choice_imp_ext_function_repr.u2 <= repr_fun_choice_imp_ext_function_repr.u0
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 1075, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
repr_fun_choice_imp_relational_choice.u1 <= repr_fun_choice_imp_relational_choice.u0
repr_fun_choice_imp_relational_choice.u2 <= repr_fun_choice_imp_relational_choice.u0
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 1102, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
setoid_fun_choice_iff_gen_setoid_fun_choice.u0 <= gen_setoid_fun_choice_imp_setoid_fun_choice.u0
setoid_fun_choice_iff_gen_setoid_fun_choice.u0 <= setoid_fun_choice_imp_gen_setoid_fun_choice.u0
setoid_fun_choice_iff_gen_setoid_fun_choice.u1 <= gen_setoid_fun_choice_imp_setoid_fun_choice.u1
setoid_fun_choice_iff_gen_setoid_fun_choice.u1 <= setoid_fun_choice_imp_gen_setoid_fun_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 1125, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
setoid_fun_choice_iff_simple_setoid_fun_choice.u0 <= setoid_fun_choice_imp_simple_setoid_fun_choice.u0
setoid_fun_choice_iff_simple_setoid_fun_choice.u0 <= simple_setoid_fun_choice_imp_setoid_fun_choice.u0
setoid_fun_choice_iff_simple_setoid_fun_choice.u1 <= setoid_fun_choice_imp_simple_setoid_fun_choice.u1
setoid_fun_choice_iff_simple_setoid_fun_choice.u1 <= simple_setoid_fun_choice_imp_setoid_fun_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 1147, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
setoid_fun_choice_imp_functional_rel_reification.u0 <= fun_choice_imp_functional_rel_reification.u0
setoid_fun_choice_imp_functional_rel_reification.u0 <= setoid_fun_choice_imp_fun_choice.u0
setoid_fun_choice_imp_functional_rel_reification.u1 <= fun_choice_imp_functional_rel_reification.u1
setoid_fun_choice_imp_functional_rel_reification.u1 <= setoid_fun_choice_imp_fun_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 1154, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
setoid_fun_choice_imp_repr_fun_choice.u2 <= setoid_fun_choice_imp_repr_fun_choice.u0
setoid_fun_choice_imp_repr_fun_choice.u2 <= setoid_fun_choice_imp_repr_fun_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 1173, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u3 <= functional_rel_reification_and_rel_choice_imp_fun_choice.u0
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u3 <= repr_fun_choice_imp_relational_choice.u0
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u3 <= repr_fun_choice_imp_relational_choice.u1
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u3 <= functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u0
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u4 <= functional_rel_reification_and_rel_choice_imp_fun_choice.u1
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u4 <= repr_fun_choice_imp_relational_choice.u2
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u4 <= functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u1
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u2 = repr_fun_choice_imp_relational_choice.u0
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 1183, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice.u0 <= setoid_fun_choice_imp_functional_rel_reification.u0
functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice.u0 <= functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice.u3
functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice.u1 <= setoid_fun_choice_imp_functional_rel_reification.u1
functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice.u1 <= functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice.u4
functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice.u3 <= functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u3
functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice.u4 <= functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u4
setoid_fun_choice_imp_repr_fun_choice.u0 = functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice.u3
setoid_fun_choice_imp_repr_fun_choice.u1 = functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice.u4
setoid_fun_choice_imp_repr_fun_choice.u2 = functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u2
setoid_fun_choice_imp_repr_fun_choice.u2 = functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice.u2
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u0 = functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice.u0
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u1 = functional_rel_reification_and_repr_fun_choice_iff_setoid_fun_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 1243, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice.u4 <= Coq.Init.Specif.16
fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice.u4 <= fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice.u0
fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice.u4 <= fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice.u1
fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice.u4 <= fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice.u2
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 1259, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u0 <= setoid_functional_choice_first_characterization.u0
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u1 <= setoid_functional_choice_first_characterization.u1
setoid_functional_choice_first_characterization.u0 <= setoid_fun_choice_imp_fun_choice.u0
setoid_functional_choice_first_characterization.u0 <= setoid_functional_choice_first_characterization.u4
setoid_functional_choice_first_characterization.u1 <= setoid_fun_choice_imp_fun_choice.u1
setoid_functional_choice_first_characterization.u1 <= setoid_functional_choice_first_characterization.u5
repr_fun_choice_imp_ext_function_repr.u0 = repr_fun_choice_imp_excluded_middle.u0
repr_fun_choice_imp_ext_function_repr.u0 = setoid_fun_choice_imp_repr_fun_choice.u2
repr_fun_choice_imp_ext_function_repr.u1 = fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice.u2
repr_fun_choice_imp_ext_function_repr.u1 = setoid_functional_choice_first_characterization.u2
repr_fun_choice_imp_ext_function_repr.u2 = fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice.u3
repr_fun_choice_imp_ext_function_repr.u2 = setoid_functional_choice_first_characterization.u3
setoid_fun_choice_imp_repr_fun_choice.u0 = setoid_functional_choice_first_characterization.u4
setoid_fun_choice_imp_repr_fun_choice.u1 = setoid_functional_choice_first_characterization.u5
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u2 = fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice.u4
fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice.u0 = setoid_functional_choice_first_characterization.u0
fun_choice_and_ext_functions_repr_and_excluded_middle_imp_setoid_fun_choice.u1 = setoid_functional_choice_first_characterization.u1
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 1298, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice.u3 <= Coq.Init.Specif.16
fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice.u3 <= fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice.u0
fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice.u3 <= fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice.u1
fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice.u3 <= fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice.u2
[private-mono,fragile,default]
File "./theories/Logic/ChoiceFacts.v", line 1315, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u0 <= setoid_functional_choice_second_characterization.u0
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u1 <= setoid_functional_choice_second_characterization.u1
setoid_functional_choice_second_characterization.u0 <= setoid_fun_choice_imp_fun_choice.u0
setoid_functional_choice_second_characterization.u0 <= setoid_functional_choice_second_characterization.u3
setoid_functional_choice_second_characterization.u1 <= setoid_fun_choice_imp_fun_choice.u1
setoid_functional_choice_second_characterization.u1 <= setoid_functional_choice_second_characterization.u4
repr_fun_choice_imp_ext_pred_repr.u0 = repr_fun_choice_imp_excluded_middle.u0
repr_fun_choice_imp_ext_pred_repr.u0 = setoid_fun_choice_imp_repr_fun_choice.u2
repr_fun_choice_imp_ext_pred_repr.u1 = fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice.u2
repr_fun_choice_imp_ext_pred_repr.u1 = setoid_functional_choice_second_characterization.u2
setoid_fun_choice_imp_repr_fun_choice.u0 = setoid_functional_choice_second_characterization.u3
setoid_fun_choice_imp_repr_fun_choice.u1 = setoid_functional_choice_second_characterization.u4
functional_rel_reification_and_repr_fun_choice_imp_setoid_fun_choice.u2 = fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice.u3
fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice.u0 = setoid_functional_choice_second_characterization.u0
fun_choice_and_ext_pred_ext_and_proof_irrel_imp_setoid_fun_choice.u1 = setoid_functional_choice_second_characterization.u1
[private-mono,fragile,default]
File "./theories/Logic/IndefiniteDescription.v", line 30, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
constructive_definite_description.u0 <= constructive_indefinite_description.u0
[private-mono,fragile,default]
File "./theories/Logic/IndefiniteDescription.v", line 39, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
constructive_indefinite_description.u0 = constructive_indefinite_descr_fun_choice.u0
constructive_indefinite_descr_fun_choice.u1 = functional_choice.u0
constructive_indefinite_descr_fun_choice.u2 = functional_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ClassicalChoice.v", line 40, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
singleton_choice.u0 <= relational_choice.u1 [private-mono,fragile,default]
File "./theories/Logic/ClassicalChoice.v", line 51, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
choice.u0 <= relational_choice.u0
choice.u0 <= unique_choice.u0
choice.u0 <= functional_rel_reification_and_rel_choice_imp_fun_choice.u0
choice.u1 <= relational_choice.u1
choice.u1 <= unique_choice.u1
choice.u1 <= functional_rel_reification_and_rel_choice_imp_fun_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ClassicalEpsilon.v", line 34, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
constructive_definite_description.u0 <= constructive_indefinite_description.u0
[private-mono,fragile,default]
File "./theories/Logic/ClassicalEpsilon.v", line 41, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
constructive_definite_descr_excluded_middle.u0 = constructive_definite_description.u0
[private-mono,fragile,default]
File "./theories/Logic/ClassicalEpsilon.v", line 102, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
choice.u1 <= constructive_indefinite_description.u0
choice.u1 <= Coq.Init.Specif.16 [private-mono,fragile,default]
File "./theories/Logic/Epsilon.v", line 30, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
epsilon_statement.u0 = epsilon_imp_constructive_indefinite_description.u0
epsilon_imp_constructive_indefinite_description.u1 = constructive_indefinite_description.u0
[private-mono,fragile,default]
File "./theories/Logic/Epsilon.v", line 38, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
SmallDrinker'sParadox.u0 = small_drinkers'_paradox.u0
[private-mono,fragile,default]
File "./theories/Logic/Epsilon.v", line 45, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iota_statement.u0 <= epsilon_statement.u0 [private-mono,fragile,default]
File "./theories/Logic/Epsilon.v", line 53, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
iota_statement.u0 = iota_imp_constructive_definite_description.u0
iota_imp_constructive_definite_description.u1 = constructive_definite_description.u0
[private-mono,fragile,default]
File "./theories/Logic/Diaconescu.v", line 90, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Logic.Diaconescu.3 = rel_choice_and_proof_irrel_imp_guarded_rel_choice.u0
Coq.Logic.Diaconescu.4 = rel_choice_and_proof_irrel_imp_guarded_rel_choice.u1
rel_choice_and_proof_irrel_imp_guarded_rel_choice.u2 = guarded_rel_choice.u0
rel_choice_and_proof_irrel_imp_guarded_rel_choice.u3 = guarded_rel_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/Diaconescu.v", line 233, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Logic.Diaconescu.13 <= ex.u0
Coq.Logic.Diaconescu.13 <= Coq.Logic.Diaconescu.11
[private-mono,fragile,default]
File "./theories/Logic/Diaconescu.v", line 265, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Logic.Diaconescu.13 <= rel_choice_and_proof_irrel_imp_guarded_rel_choice.u2
Coq.Logic.Diaconescu.11 = rel_choice_and_proof_irrel_imp_guarded_rel_choice.u0
Coq.Logic.Diaconescu.12 = rel_choice_and_proof_irrel_imp_guarded_rel_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/ClassicalDescription.v", line 34, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
constructive_definite_descr_excluded_middle.u0 = constructive_definite_description.u0
[private-mono,fragile,default]
File "./theories/Logic/ClassicalDescription.v", line 48, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
classical_definite_description.u0 <= constructive_definite_description.u0
[private-mono,fragile,default]
File "./theories/Logic/ClassicalDescription.v", line 71, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
dependent_unique_choice.u1 <= constructive_definite_description.u0
dependent_unique_choice.u1 <= Coq.Init.Specif.16
[private-mono,fragile,default]
File "./theories/Logic/ClassicalDescription.v", line 80, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
unique_choice.u0 <= dependent_unique_choice.u0
unique_choice.u1 <= dependent_unique_choice.u1 [private-mono,fragile,default]
File "./theories/Logic/SetoidChoice.v", line 54, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
choice.u0 = setoid_functional_choice_first_characterization.u0
choice.u1 = setoid_functional_choice_first_characterization.u1
setoid_functional_choice_first_characterization.u2 = extensional_function_representative.u0
setoid_functional_choice_first_characterization.u3 = extensional_function_representative.u1
setoid_functional_choice_first_characterization.u4 = setoid_choice.u0
setoid_functional_choice_first_characterization.u5 = setoid_choice.u1
[private-mono,fragile,default]
File "./theories/Logic/SetoidChoice.v", line 62, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
setoid_fun_choice_imp_repr_fun_choice.u2 = representative_choice.u0
[private-mono,fragile,default]
File "./theories/MSets/MSetGenTree.v", line 864, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fold_spec.u0 <= fold_spec'.u0 [private-mono,fragile,default]
File "./theories/ZArith/Znumtheory.v", line 190, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
hypo.u0 < list.u0 [private-mono,fragile,default]
File "./theories/micromega/RingMicromega.v", line 113, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.micromega.RingMicromega.1 <= Coq.micromega.OrderedRing.21
[private-mono,fragile,default]
File "./theories/micromega/RingMicromega.v", line 624, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.micromega.RingMicromega.2 <= make_conj.u0
Coq.micromega.RingMicromega.2 <= make_conj_impl.u0
Coq.micromega.RingMicromega.2 <= make_conj_in.u0
[private-mono,fragile,default]
File "./theories/micromega/RingMicromega.v", line 918, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
cnf_normalise_correct.u0 <= cnf_of_list_correct.u0
[private-mono,fragile,default]
File "./theories/micromega/RingMicromega.v", line 934, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
cnf_negate_correct.u0 <= cnf_of_list_correct.u0
[private-mono,fragile,default]
File "./theories/micromega/ZCoeff.v", line 93, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.micromega.ZCoeff.1 <= Coq.micromega.RingMicromega.1
[private-mono,fragile,default]
File "./theories/MSets/MSetPositive.v", line 313, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= rewrite_relation_eq_dom.u0
t.u0 <= rewrite_relation_eq_dom.u1
t.u0 <= Coq.Classes.Morphisms.51 [private-mono,fragile,default]
File "./theories/MSets/MSetPositive.v", line 581, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= Morphisms_Prop.all_iff_morphism_obligation_1.u0
t.u0 <= all.u0 [private-mono,fragile,default]
File "./theories/MSets/MSetPositive.v", line 925, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
elt.u0 <= Coq.Sorting.Sorted.1 [private-mono,fragile,default]
File "./theories/setoid_ring/Ncring_initial.v", line 117, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.Ncring_initial.1 <= Coq.setoid_ring.Ncring.274
One.u0 <= one_notation.u0 [private-mono,fragile,default]
File "./theories/FSets/FSetPositive.v", line 319, characters 35-39:
Warning: Adding constraints to the global env from Qed body:
elt.u0 <= Coq.Classes.Morphisms.1
elt.u0 <= Coq.Classes.RelationClasses.1
elt.u0 <= rewrite_relation_eq_dom.u1
elt.u0 <= Coq.Classes.Morphisms.51
t.u0 <= Coq.Classes.Morphisms.1
t.u0 <= Coq.Classes.RelationClasses.1
t.u0 <= eq.u0
t.u0 <= rewrite_relation_eq_dom.u0
t.u0 <= rewrite_relation_eq_dom.u1
t.u0 <= Coq.Classes.Morphisms.51 [private-mono,fragile,default]
File "./theories/FSets/FSetPositive.v", line 615, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= Morphisms_Prop.all_iff_morphism_obligation_1.u0
t.u0 <= all.u0 [private-mono,fragile,default]
File "./theories/FSets/FSetPositive.v", line 1015, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
elt.u0 <= Coq.Lists.SetoidList.1
elt.u0 <= Coq.Sorting.Sorted.1 [private-mono,fragile,default]
File "./theories/FSets/FSetFacts.v", line 404, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= Coq.Classes.Morphisms.51 [private-mono,fragile,default]
File "./theories/MSets/MSetFacts.v", line 510, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
E.t.u0 <= Coq.Classes.Morphisms.95
E.t.u0 <= flip_arrow.u0
t.u0 <= Coq.Classes.Morphisms.95
t.u0 <= flip_arrow.u0
t.u0 <= flip_arrow.u1 [private-mono,fragile,default]
File "./theories/setoid_ring/Field_theory.v", line 69, characters 41-45:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.Field_theory.1 <= Coq.setoid_ring.Ring_theory.100
[private-mono,fragile,default]
File "./theories/setoid_ring/Field_theory.v", line 190, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
hypo.u0 < list.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 106, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.14 <= eq_option_alt.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 147, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.14 <= MapsTo_fun.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 241, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.14 <= map_1.u0
Coq.FSets.FMapFacts.14 <= map_1.u1
Coq.FSets.FMapFacts.14 <= map_2.u0
Coq.FSets.FMapFacts.14 <= map_2.u1 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 258, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.14 <= mapi_1.u0
Coq.FSets.FMapFacts.14 <= mapi_1.u1
Coq.FSets.FMapFacts.14 <= mapi_2.u0
Coq.FSets.FMapFacts.14 <= mapi_2.u1 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 331, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
mem_find_b.u0 <= Coq.FSets.FMapFacts.14 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 343, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.27 <= Coq.FSets.FMapFacts.14
[private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 390, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.27 <= mem_find_b.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 516, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.27 <= map2_1.u0
Coq.FSets.FMapFacts.27 <= map2_1.u1
Coq.FSets.FMapFacts.27 <= map2_1.u2
Coq.FSets.FMapFacts.27 <= map2_2.u0
Coq.FSets.FMapFacts.27 <= map2_2.u1
Coq.FSets.FMapFacts.27 <= map2_2.u2 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 567, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.66 <= eq_option_alt.u0
Coq.FSets.FMapFacts.66 <= Coq.FSets.FMapFacts.14
[private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 649, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Equal_ST.u0 <= Equal_refl.u0
Equal_ST.u0 <= Equal_sym.u0
Equal_ST.u0 <= Equal_trans.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 670, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
In_m_Proper.u0 <= Coq.FSets.FMapFacts.14 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 678, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
MapsTo_m_Proper.u0 <= Coq.FSets.FMapFacts.14 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 686, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
t.u1 <= Coq.Classes.Morphisms.51
Empty_m_Proper.u0 <= EqualSetoid_Symmetric.u0
Empty_m_Proper.u0 <= MapsTo_m_Proper.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 693, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
is_empty_m_Proper.u0 <= Coq.FSets.FMapFacts.14
is_empty_m_Proper.u0 <= Empty_m_Proper.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 700, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
mem_m_Proper.u0 <= Coq.FSets.FMapFacts.14
mem_m_Proper.u0 <= EqualSetoid_Reflexive.u0
mem_m_Proper.u0 <= In_m_Proper.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 707, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
find_m_Proper.u0 <= eq_option_alt.u0
find_m_Proper.u0 <= Coq.FSets.FMapFacts.14
find_m_Proper.u0 <= EqualSetoid_Reflexive.u0
find_m_Proper.u0 <= MapsTo_m_Proper.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 716, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
add_m_Proper.u0 <= Coq.FSets.FMapFacts.27 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 725, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
remove_m_Proper.u0 <= Coq.FSets.FMapFacts.27 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 732, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
map_m_Proper.u0 <= Coq.FSets.FMapFacts.27
map_m_Proper.u0 <= find_m_Proper.u0
map_m_Proper.u1 <= Coq.FSets.FMapFacts.27 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 780, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.148 <= Coq.FSets.FMapFacts.27
[private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 920, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
E.t.u0 <= fold_left_rev_right.u0
Coq.FSets.FMapFacts.148 <= fold_left_rev_right.u0
fold_spec_right.u0 <= fold_1.u0
fold_spec_right.u0 <= fold_left_rev_right.u1 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 973, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
t.u1 <= Coq.Init.Datatypes.51
fold_rec.u0 <= Coq.Init.Datatypes.51
fold_rec.u0 <= uncurry.u2
fold_rec.u0 <= fold_spec_right.u0
fold_rec.u0 <= Coq.Lists.List.418
fold_rec.u1 <= eq_rect_r.u0
fold_rec.u1 <= Coq.Init.Datatypes.51 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 993, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_rec_bis.u0 <= fold_rec.u0
fold_rec_bis.u1 <= fold_rec.u1 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1001, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_rec_nodep.u0 <= fold_rec_bis.u0
fold_rec_nodep.u1 <= fold_rec_bis.u1 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1016, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_rec_weak.u0 <= fold_rec_bis.u0
fold_rec_weak.u1 <= fold_rec_bis.u1 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1035, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_rel.u0 <= Coq.Init.Datatypes.51
fold_rel.u0 <= uncurry.u2
fold_rel.u0 <= fold_spec_right.u0
fold_rel.u0 <= Coq.Lists.List.418
fold_rel.u1 <= Coq.Init.Datatypes.51
fold_rel.u1 <= uncurry.u2
fold_rel.u1 <= fold_spec_right.u0
fold_rel.u1 <= Coq.Lists.List.418
fold_rel.u2 <= eq_rect_r.u0
fold_rel.u2 <= Coq.Init.Datatypes.51 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1047, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
map_induction.u0 <= fold_rec.u1 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1058, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
map_induction_bis.u0 <= fold_rec_bis.u1 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1072, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
t.u1 <= fold_rec.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1093, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.303 <= fold_rel.u0
Coq.FSets.FMapFacts.303 <= fold_rel.u1 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1101, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.303 <= fold_rec_nodep.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1135, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.148 <= EqualSetoid_Reflexive.u0
Coq.FSets.FMapFacts.148 <= In_m_Proper.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1159, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.148 <= find_m_Proper.u0
Coq.FSets.FMapFacts.303 <= Coq.Lists.SetoidList.109
[private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1182, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.303 <= Coq.Classes.Morphisms.51
Coq.FSets.FMapFacts.303 <= Coq.Lists.SetoidList.136
[private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1235, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
E.t.u0 <= fold_left_S_O.u0
Coq.FSets.FMapFacts.148 <= fold_left_S_O.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1588, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.148 <= EqualSetoid.u0
Coq.FSets.FMapFacts.148 <= remove_m_Proper.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1678, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.148 <= Coq.FSets.FMapFacts.66
Coq.FSets.FMapFacts.148 <= mem_m_Proper.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1774, characters 44-48:
Warning: Adding constraints to the global env from Qed body:
cardinal_m_Proper.u0 <= Coq.FSets.FMapFacts.148
[private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1782, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
Disjoint_m_Proper.u0 <= EqualSetoid_Symmetric.u0
[private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1792, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
Partition_m_Proper.u0 <= EqualSetoid_Symmetric.u0
Partition_m_Proper.u0 <= Disjoint_m_Proper.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1805, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
t.u1 <= default_relation.u0
t.u1 <= equivalence_default.u0
t.u1 <= Coq.FSets.FMapFacts.303
update_m_Proper.u0 <= EqualSetoid_Transitive.u0
update_m_Proper.u0 <= add_m_Proper.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1824, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
restrict_m_Proper.u0 <= EqualSetoid_Transitive.u0
restrict_m_Proper.u0 <= add_m_Proper.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1843, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
diff_m_Proper.u0 <= EqualSetoid_Transitive.u0
diff_m_Proper.u0 <= add_m_Proper.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1940, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFacts.565 <= Coq.FSets.FMapInterface.36
Coq.Structures.OrderedType.87 = Coq.FSets.FMapInterface.36
[private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 1984, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Structures.OrderedType.87 = Coq.FSets.FMapInterface.6
[private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 2212, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
t.u1 <= Coq.Init.Datatypes.9
map_induction_max.u0 <= Coq.Init.Datatypes.9 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 2239, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
map_induction_min.u0 <= Coq.Init.Datatypes.9 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 2259, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_Equal.u0 <= Coq.Lists.SetoidList.109
fold_Equal.u0 <= uncurry.u2
fold_Equal.u0 <= fold_spec_right.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 2274, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_Add_Above.u0 <= Coq.Lists.SetoidList.109
fold_Add_Above.u0 <= uncurry.u2
fold_Add_Above.u0 <= fold_spec_right.u0
fold_Add_Above.u0 <= Coq.Lists.List.418 [private-mono,fragile,default]
File "./theories/FSets/FMapFacts.v", line 2290, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_Add_Below.u0 <= Coq.Lists.SetoidList.109
fold_Add_Below.u0 <= uncurry.u2
fold_Add_Below.u0 <= fold_spec_right.u0
fold_Add_Below.u0 <= Coq.Lists.List.418
fold_Add_Below.u0 <= fold_right_app.u1 [private-mono,fragile,default]
File "./theories/micromega/QMicromega.v", line 273, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.micromega.RingMicromega.2 <= make_impl_map.u0
[private-mono,fragile,default]
File "./theories/QArith/Qcabs.v", line 39, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Qcabs_case.u0 <= Qabs_case.u0 [private-mono,fragile,default]
File "./theories/micromega/ZMicromega.v", line 504, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
normalise_correct.u0 <= cnf_of_list_correct.u0 [private-mono,fragile,default]
File "./theories/micromega/ZMicromega.v", line 548, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
negate_correct.u0 <= cnf_of_list_correct.u0 [private-mono,fragile,default]
File "./theories/micromega/ZMicromega.v", line 842, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.micromega.RingMicromega.2 = Coq.micromega.EnvRing.10
[private-mono,fragile,default]
File "./theories/micromega/ZMicromega.v", line 1845, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.micromega.RingMicromega.2 <= make_impl_map.u0
[private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 351, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
E.t.u0 <= fold_left_rev_right.u0
fold_spec_right.u0 <= fold_1.u0
fold_spec_right.u0 <= fold_left_rev_right.u1 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 392, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= Coq.Init.Datatypes.51
fold_rec.u0 <= fold_spec_right.u0
fold_rec.u0 <= Coq.Init.Datatypes.51
fold_rec.u0 <= Coq.Lists.List.418
fold_rec.u1 <= eq_rect_r.u0
fold_rec.u1 <= Coq.Init.Datatypes.51 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 409, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_rec_bis.u0 <= fold_rec.u0
fold_rec_bis.u1 <= fold_rec.u1 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 417, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_rec_nodep.u0 <= fold_rec_bis.u0
fold_rec_nodep.u1 <= fold_rec_bis.u1 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 432, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_rec_weak.u0 <= fold_rec_bis.u0
fold_rec_weak.u1 <= fold_rec_bis.u1 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 447, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_rel.u0 <= fold_spec_right.u0
fold_rel.u0 <= Coq.Init.Datatypes.51
fold_rel.u0 <= Coq.Lists.List.418
fold_rel.u1 <= fold_spec_right.u0
fold_rel.u1 <= Coq.Init.Datatypes.51
fold_rel.u1 <= Coq.Lists.List.418
fold_rel.u2 <= eq_rect_r.u0
fold_rel.u2 <= Coq.Init.Datatypes.51 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 459, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
set_induction.u0 <= fold_rec.u1 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 470, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
set_induction_bis.u0 <= fold_rec_bis.u1 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 479, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= fold_rec.u0 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 503, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_0.u0 <= fold_spec_right.u0 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 520, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_1.u0 <= fold_0.u0
fold_1.u0 <= Coq.Lists.List.418 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 536, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_2.u0 <= fold_0.u0 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 548, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_1b.u0 <= M.fold_1.u0 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 562, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FSetProperties.86 <= fold_rel.u0
Coq.FSets.FSetProperties.86 <= fold_rel.u1 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 586, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FSetProperties.86 <= fold_1.u0
Coq.FSets.FSetProperties.86 <= fold_2.u0 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 593, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FSetProperties.86 <= fold_1b.u0 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 704, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
E.t.u0 <= fold_left_S_O.u0 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 1085, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= Coq.Init.Datatypes.9
set_induction_max.u0 <= Coq.Init.Logic.2
set_induction_max.u0 <= Coq.Init.Datatypes.9 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 1106, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
set_induction_min.u0 <= Coq.Init.Logic.2
set_induction_min.u0 <= Coq.Init.Datatypes.9 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 1124, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_3.u0 <= fold_spec_right.u0
fold_3.u0 <= Coq.Lists.SetoidList.109
fold_3.u0 <= Coq.Lists.List.418 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 1141, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_4.u0 <= fold_1.u0
fold_4.u0 <= Coq.Lists.SetoidList.109
fold_4.u0 <= Coq.Lists.List.414
fold_4.u0 <= fold_left_rev_right.u1 [private-mono,fragile,default]
File "./theories/FSets/FSetProperties.v", line 1159, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FSetProperties.222 <= fold_spec_right.u0
Coq.FSets.FSetProperties.222 <= Coq.Lists.SetoidList.109
[private-mono,fragile,default]
File "./theories/Sorting/PermutSetoid.v", line 535, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.PermutSetoid.149 <= Coq.Sorting.Permutation.32
[private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 354, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
E.t.u0 <= fold_left_rev_right.u0
fold_spec_right.u0 <= fold_spec.u0
fold_spec_right.u0 <= fold_left_rev_right.u1 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 392, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_rec.u0 <= fold_spec_right.u0
fold_rec.u0 <= Coq.Init.Datatypes.51
fold_rec.u0 <= Coq.Lists.List.418
fold_rec.u1 <= eq_rect_r.u0
fold_rec.u1 <= Coq.Init.Datatypes.51 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 409, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_rec_bis.u0 <= fold_rec.u0
fold_rec_bis.u1 <= fold_rec.u1 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 417, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_rec_nodep.u0 <= fold_rec_bis.u0
fold_rec_nodep.u1 <= fold_rec_bis.u1 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 432, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_rec_weak.u0 <= fold_rec_bis.u0
fold_rec_weak.u1 <= fold_rec_bis.u1 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 447, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_rel.u0 <= fold_spec_right.u0
fold_rel.u0 <= Coq.Init.Datatypes.51
fold_rel.u0 <= Coq.Lists.List.418
fold_rel.u1 <= fold_spec_right.u0
fold_rel.u1 <= Coq.Init.Datatypes.51
fold_rel.u1 <= Coq.Lists.List.418
fold_rel.u2 <= eq_rect_r.u0
fold_rel.u2 <= Coq.Init.Datatypes.51 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 459, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
set_induction.u0 <= fold_rec.u1 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 470, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
set_induction_bis.u0 <= fold_rec_bis.u1 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 479, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= fold_rec.u0 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 501, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_0.u0 <= fold_spec_right.u0 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 518, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_1.u0 <= fold_0.u0
fold_1.u0 <= Coq.Lists.List.418 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 535, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_2.u0 <= fold_0.u0 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 547, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_1b.u0 <= fold_spec.u0 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 562, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.MSets.MSetProperties.86 <= fold_rel.u0
Coq.MSets.MSetProperties.86 <= fold_rel.u1 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 586, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.MSets.MSetProperties.86 <= fold_1.u0
Coq.MSets.MSetProperties.86 <= fold_2.u0 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 593, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.MSets.MSetProperties.86 <= fold_1b.u0 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 704, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
E.t.u0 <= fold_left_S_O.u0 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 1091, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
t.u0 <= Coq.Init.Datatypes.9
set_induction_max.u0 <= Coq.Init.Logic.2
set_induction_max.u0 <= Coq.Init.Datatypes.9 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 1112, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
set_induction_min.u0 <= Coq.Init.Datatypes.9 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 1130, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_3.u0 <= fold_spec_right.u0
fold_3.u0 <= Coq.Lists.SetoidList.109
fold_3.u0 <= Coq.Lists.List.418 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 1146, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
fold_4.u0 <= fold_spec.u0
fold_4.u0 <= flip.u2
fold_4.u0 <= Coq.Lists.SetoidList.109
fold_4.u0 <= Coq.Lists.List.414
fold_4.u0 <= fold_left_rev_right.u1 [private-mono,fragile,default]
File "./theories/MSets/MSetProperties.v", line 1165, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.MSets.MSetProperties.222 <= fold_spec_right.u0
Coq.MSets.MSetProperties.222 <= Coq.Lists.SetoidList.109
[private-mono,fragile,default]
File "./theories/FSets/FSetToFiniteSet.v", line 86, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
U.t.u0 <= Coq.Sets.Constructive_sets.1 [private-mono,fragile,default]
File "./theories/Sorting/PermutEq.v", line 152, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.PermutEq.1 <= Coq.Sorting.Permutation.32
[private-mono,fragile,default]
File "./theories/Sorting/Heap.v", line 113, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
is_heap_rect.u0 <= Coq.Sorting.Heap.3
is_heap_rect.u0 <= Coq.Init.Logic.4 [private-mono,fragile,default]
File "./theories/Sorting/Heap.v", line 191, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.Heap.1 <= Coq.Init.Specif.738 [private-mono,fragile,default]
File "./theories/Sorting/Heap.v", line 249, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.Heap.1 <= is_heap_rect.u0
Coq.Sorting.Heap.1 <= Coq.Sorting.Heap.12 [private-mono,fragile,default]
File "./theories/Sorting/Heap.v", line 274, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.Heap.1 <= Coq.Sorting.Heap.14 [private-mono,fragile,default]
File "./theories/Sorting/Heap.v", line 303, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
Coq.Sorting.Heap.1 <= Coq.Sorting.Heap.9
Coq.Sorting.Heap.1 <= Coq.Sorting.Heap.16 [private-mono,fragile,default]
File "./theories/MSets/MSetToFiniteSet.v", line 86, characters 1-5:
Warning: Adding constraints to the global env from Qed body:
U.t.u0 <= Coq.Sets.Constructive_sets.1 [private-mono,fragile,default]
File "./theories/FSets/FSetEqProperties.v", line 487, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
set_rec.u0 <= set_induction.u0 [private-mono,fragile,default]
File "./theories/FSets/FSetEqProperties.v", line 507, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FSetEqProperties.14 <= Coq.FSets.FSetProperties.86
[private-mono,fragile,default]
File "./theories/FSets/FSetEqProperties.v", line 833, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
E.t.u0 <= Coq.Init.Logic.4 [private-mono,fragile,default]
File "./theories/FSets/FSetEqProperties.v", line 935, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fold_compat.u0 <= Coq.FSets.FSetEqProperties.14
[private-mono,fragile,default]
File "./theories/Reals/Abstract/ConstructiveReals.v", line 366, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
CRlt_morph.u0 = CRlt_morph.u2
CRlt_morph.u1 = CRlt_morph.u2 [private-mono,fragile,default]
File "./theories/Reals/Abstract/ConstructiveReals.v", line 1235, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
CRapart_morph.u0 = CRapart_morph.u2
CRapart_morph.u1 = CRapart_morph.u2 [private-mono,fragile,default]
File "./theories/btauto/Reflect.v", line 180, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
list_nth_base.u0 <= Positive_as_OT.peano_rect_base.u0
[private-mono,fragile,default]
File "./theories/btauto/Reflect.v", line 188, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
list_nth_succ.u0 <= Positive_as_OT.peano_rect_succ.u0
[private-mono,fragile,default]
File "./theories/btauto/Reflect.v", line 196, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
list_nth_nil.u0 <= list_nth_base.u0
list_nth_nil.u0 <= list_nth_succ.u0 [private-mono,fragile,default]
File "./theories/btauto/Reflect.v", line 209, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
make_last_nth_1.u0 <= list_nth_base.u0
make_last_nth_1.u0 <= list_nth_succ.u0
make_last_nth_1.u0 <= list_nth_nil.u0
make_last_nth_1.u0 <= Positive_as_OT.peano_rect_succ.u0
[private-mono,fragile,default]
File "./theories/btauto/Reflect.v", line 217, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
make_last_nth_2.u0 <= list_nth_succ.u0
make_last_nth_2.u0 <= Positive_as_OT.peano_rect_succ.u0
[private-mono,fragile,default]
File "./theories/MSets/MSetEqProperties.v", line 489, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
set_rec.u0 <= set_induction.u0 [private-mono,fragile,default]
File "./theories/MSets/MSetEqProperties.v", line 509, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.MSets.MSetEqProperties.15 <= Coq.MSets.MSetProperties.86
[private-mono,fragile,default]
File "./theories/MSets/MSetEqProperties.v", line 921, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fold_compat.u0 <= Coq.MSets.MSetEqProperties.15
[private-mono,fragile,default]
File "./theories/MSets/MSetRBT.v", line 567, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
L.MO.OrderTac.TO.t.u0 <= rrmatch.u0 [private-mono,fragile,default]
File "./theories/MSets/MSetRBT.v", line 587, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
L.MO.OrderTac.TO.t.u0 <= rrmatch'.u0 [private-mono,fragile,default]
File "./theories/MSets/MSetRBT.v", line 602, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
L.MO.OrderTac.TO.t.u0 <= rmatch.u0 [private-mono,fragile,default]
File "./theories/MSets/MSetRBT.v", line 1244, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
L.MO.OrderTac.TO.t.u0 <= fold_spec.u0
L.MO.OrderTac.TO.t.u0 <= fold_left_rev_right.u0
L.MO.OrderTac.TO.t.u0 <= fold_left_rev_right.u1
[private-mono,fragile,default]
File "./theories/FSets/FMapPositive.v", line 285, characters 4-8:
Warning: Adding constraints to the global env from Qed body:
key.u0 <= Coq.Lists.List.13
Coq.FSets.FMapPositive.4 <= Coq.Lists.List.13 [private-mono,fragile,default]
File "./theories/FSets/FMapPositive.v", line 558, characters 37-41:
Warning: Adding constraints to the global env from Qed body:
key.u0 <= rewrite_relation_eq_dom.u1
key.u0 <= Coq.Classes.Morphisms.51
tree.u0 <= Coq.Classes.Morphisms.1
tree.u0 <= Coq.Classes.RelationClasses.1
tree.u0 <= rewrite_relation_eq_dom.u0
tree.u0 <= rewrite_relation_eq_dom.u1
tree.u0 <= Coq.Classes.Morphisms.51 [private-mono,fragile,default]
File "./theories/FSets/FMapPositive.v", line 596, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
tree.u0 <= eq_rewrite_relation.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapPositive.v", line 771, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
gmapi.u0 <= xgmapi.u0
gmapi.u1 <= xgmapi.u1 [private-mono,fragile,default]
File "./theories/FSets/FMapPositive.v", line 786, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
mapi_1.u0 <= gmapi.u0
mapi_1.u1 <= gmapi.u1 [private-mono,fragile,default]
File "./theories/FSets/FMapPositive.v", line 800, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
mapi_2.u0 <= gmapi.u0
mapi_2.u1 <= gmapi.u1 [private-mono,fragile,default]
File "./theories/FSets/FMapPositive.v", line 807, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
map_1.u0 <= mapi_1.u0
map_1.u1 <= mapi_1.u1 [private-mono,fragile,default]
File "./theories/FSets/FMapPositive.v", line 813, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
map_2.u0 <= mapi_2.u0
map_2.u1 <= mapi_2.u1 [private-mono,fragile,default]
File "./theories/FSets/FMapPositive.v", line 1126, characters 2-6:
Warning: Adding constraints to the global env from Qed body:
map2_commut.u0 <= xmap2_lr.u0
map2_commut.u1 <= xmap2_lr.u1 [private-mono,fragile,default]
File "./theories/Reals/Abstract/ConstructiveLimits.v", line 208, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
CR_cv_morph.u0 = CR_cv_morph.u1 [private-mono,fragile,default]
File "./theories/setoid_ring/Integral_domain.v", line 30, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.setoid_ring.Integral_domain.25 <= Coq.setoid_ring.Ncring_initial.1
Coq.setoid_ring.Integral_domain.25 <= Coq.setoid_ring.Ring_polynom.1
Coq.setoid_ring.Integral_domain.25 <= Coq.setoid_ring.Ring_theory.1
Coq.setoid_ring.Integral_domain.25 <= Coq.setoid_ring.Cring.11
Coq.setoid_ring.Integral_domain.25 <= prod.u0
Coq.setoid_ring.Integral_domain.25 <= prod.u1
Coq.setoid_ring.Integral_domain.25 <= list.u0 [private-mono,fragile,default]
File "./theories/Reals/Cauchy/ConstructiveCauchyReals.v", line 399, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
CRealLt_morph.u0 = CRealLt_morph.u2
CRealLt_morph.u1 = CRealLt_morph.u2 [private-mono,fragile,default]
File "./theories/Reals/Cauchy/ConstructiveCauchyReals.v", line 407, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
CRealGt_morph.u0 = CRealGt_morph.u2
CRealGt_morph.u1 = CRealGt_morph.u2 [private-mono,fragile,default]
File "./theories/Reals/Cauchy/ConstructiveCauchyReals.v", line 422, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
CReal_appart_morph.u0 = CReal_appart_morph.u2
CReal_appart_morph.u1 = CReal_appart_morph.u2 [private-mono,fragile,default]
File "./theories/nsatz/NsatzTactic.v", line 46, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.nsatz.NsatzTactic.1 <= Coq.setoid_ring.Ncring_initial.1
Coq.nsatz.NsatzTactic.1 <= Coq.setoid_ring.Ring_polynom.1
Coq.nsatz.NsatzTactic.1 <= Coq.setoid_ring.Ring_theory.1
Coq.nsatz.NsatzTactic.1 <= default_relation.u0
Coq.nsatz.NsatzTactic.1 <= equivalence_default.u0
Coq.nsatz.NsatzTactic.1 <= Coq.setoid_ring.Cring.11
Coq.nsatz.NsatzTactic.1 <= prod.u0
Coq.nsatz.NsatzTactic.1 <= prod.u1
Coq.nsatz.NsatzTactic.1 <= list.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapAVL.v", line 602, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapAVL.259 <= eq.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapAVL.v", line 1438, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fold_equiv.u0 <= fold_equiv_aux.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapAVL.v", line 1449, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
fold_1.u0 <= L.fold_1.u0
fold_1.u0 <= fold_equiv.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapAVL.v", line 1566, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapAVL.597 <= eq.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapAVL.v", line 1595, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapAVL.600 <= eq.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapAVL.v", line 1629, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapAVL.603 <= Coq.FSets.FMapAVL.259 [private-mono,fragile,default]
File "./theories/FSets/FMapAVL.v", line 1720, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapAVL.610 <= Coq.FSets.FMapAVL.259 [private-mono,fragile,default]
File "./theories/FSets/FMapAVL.v", line 1813, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapAVL.644 <= Coq.FSets.FMapAVL.603
Coq.FSets.FMapAVL.644 <= Coq.FSets.FMapAVL.610 [private-mono,fragile,default]
File "./theories/FSets/FMapAVL.v", line 1934, characters 59-63:
Warning: Adding constraints to the global env from Qed body:
Raw.Proofs.fold_1.u0 = fold_1.u0 [private-mono,fragile,default]
File "./theories/FSets/FMapFullAVL.v", line 442, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Coq.FSets.FMapFullAVL.73 <= Coq.FSets.FMapFullAVL.61
Coq.FSets.FMapFullAVL.73 <= Coq.FSets.FMapFullAVL.64
[private-mono,fragile,default]
File "./theories/FSets/FMapFullAVL.v", line 550, characters 59-63:
Warning: Adding constraints to the global env from Qed body:
Proofs.fold_1.u0 = fold_1.u0 [private-mono,fragile,default]
File "./theories/Reals/Cauchy/ConstructiveRcomplete.v", line 65, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
seq_cv_morph.u0 = seq_cv_morph.u1 [private-mono,fragile,default]
File "./theories/Reals/PSeries_reg.v", line 611, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Metric_Space.u0 <= list.u0 [private-mono,fragile,default]
File "./theories/Reals/RiemannInt_SF.v", line 235, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
is_subdivision.u0 <= Coq.Init.Specif.10 [private-mono,fragile,default]
File "./theories/Reals/RiemannInt_SF.v", line 1709, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
IsStepFun.u0 <= Coq.Init.Specif.3
IsStepFun.u0 <= Coq.Init.Datatypes.51 [private-mono,fragile,default]
File "./theories/Reals/RiemannInt_SF.v", line 1980, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
IsStepFun.u0 <= Coq.Init.Logic.2 [private-mono,fragile,default]
File "./theories/Reals/RiemannInt_SF.v", line 2298, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
IsStepFun.u0 <= Coq.Init.Logic.4
IsStepFun.u0 <= Coq.Init.Specif.10 [private-mono,fragile,default]
File "./theories/Reals/RiemannInt.v", line 206, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
IsStepFun.u0 <= Coq.Init.Specif.16 [private-mono,fragile,default]
File "./theories/Reals/RiemannInt.v", line 810, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Riemann_integrable.u0 <= Coq.Init.Logic.2
Riemann_integrable.u0 <= eq_rect_r.u0 [private-mono,fragile,default]
File "./theories/Reals/RiemannInt.v", line 978, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
IsStepFun.u0 <= ex.u0 [private-mono,fragile,default]
File "./theories/Reals/NewtonInt.v", line 550, characters 0-4:
Warning: Adding constraints to the global env from Qed body:
Newton_integrable.u0 <= Coq.Init.Specif.3
Newton_integrable.u0 <= Coq.Init.Logic.10
Newton_integrable.u0 <= eq_rect_r.u0 [private-mono,fragile,default]