aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES.md5
-rw-r--r--plugins/nsatz/Nsatz.v3
-rw-r--r--plugins/setoid_ring/Ncring_initial.v1
-rw-r--r--plugins/setoid_ring/Ncring_tac.v18
-rw-r--r--plugins/setoid_ring/Rings_Q.v1
-rw-r--r--plugins/setoid_ring/Rings_R.v1
-rw-r--r--test-suite/bugs/closed/HoTT_coq_056.v4
-rw-r--r--test-suite/bugs/closed/bug_3324.v4
-rw-r--r--test-suite/bugs/closed/bug_3454.v6
-rw-r--r--test-suite/bugs/closed/bug_3682.v2
-rw-r--r--test-suite/bugs/closed/bug_4782.v4
-rw-r--r--test-suite/bugs/closed/bug_5401.v2
-rw-r--r--test-suite/success/Typeclasses.v12
-rw-r--r--test-suite/success/auto.v10
-rw-r--r--test-suite/success/bteauto.v8
-rw-r--r--test-suite/success/destruct.v2
-rw-r--r--test-suite/success/eauto.v12
-rw-r--r--test-suite/success/setoid_test2.v4
-rw-r--r--theories/Classes/CRelationClasses.v7
-rw-r--r--theories/Classes/RelationClasses.v4
-rw-r--r--theories/Classes/RelationPairs.v3
-rw-r--r--theories/Classes/SetoidTactics.v1
-rw-r--r--vernac/classes.ml4
23 files changed, 80 insertions, 38 deletions
diff --git a/CHANGES.md b/CHANGES.md
index bcdb951a94..d041f54173 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -101,6 +101,11 @@ Vernacular commands
- Option `Refine Instance Mode` has been turned off by default, meaning that
`Instance` no longer opens a proof when a body is provided.
+- `Instance`, when no body is provided, now always opens a proof. This is a
+ breaking change, as instance of `Instance foo : C.` where `C` is a trivial
+ class will have to be changed into `Instance foo : C := {}.` or
+ `Instance foo : C. Proof. Qed.`.
+
Tools
- The `-native-compiler` flag of `coqc` and `coqtop` now takes an argument which can have three values:
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index c5a09d677e..a964febf9c 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -452,6 +452,7 @@ constructor;red;intros;subst;trivial.
Qed.
Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)).
+Defined.
Instance Rri : (Ring (Ro:=Rops)).
constructor;
@@ -468,6 +469,7 @@ Class can_compute_Z (z : Z) := dummy_can_compute_Z : True.
Hint Extern 0 (can_compute_Z ?v) =>
match isZcst v with true => exact I end : typeclass_instances.
Instance reify_IZR z lvar {_ : can_compute_Z z} : reify (PEc z) lvar (IZR z).
+Defined.
Lemma R_one_zero: 1%R <> 0%R.
discrR.
@@ -484,6 +486,7 @@ exact Rmult_integral. exact R_one_zero. Defined.
Require Import QArith.
Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq).
+Defined.
Instance Qri : (Ring (Ro:=Qops)).
constructor.
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 1ca6227f25..aa0370b2ac 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -32,6 +32,7 @@ Lemma Zsth : Equivalence (@eq Z).
Proof. exact Z.eq_equiv. Qed.
Instance Zops:@Ring_ops Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z).
+Defined.
Instance Zr: (@Ring _ _ _ _ _ _ _ _ Zops).
Proof.
diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v
index 7958507819..c8d560cfe9 100644
--- a/plugins/setoid_ring/Ncring_tac.v
+++ b/plugins/setoid_ring/Ncring_tac.v
@@ -27,41 +27,50 @@ Class nth (R:Type) (t:R) (l:list R) (i:nat).
Instance Ifind0 (R:Type) (t:R) l
: nth t(t::l) 0.
+Defined.
Instance IfindS (R:Type) (t2 t1:R) l i
{_:nth t1 l i}
: nth t1 (t2::l) (S i) | 1.
+Defined.
Class closed (T:Type) (l:list T).
Instance Iclosed_nil T
: closed (T:=T) nil.
+Defined.
Instance Iclosed_cons T t (l:list T)
{_:closed l}
: closed (t::l).
+Defined.
Class reify (R:Type)`{Rr:Ring (T:=R)} (e:PExpr Z) (lvar:list R) (t:R).
Instance reify_zero (R:Type) lvar op
`{Ring (T:=R)(ring0:=op)}
: reify (ring0:=op)(PEc 0%Z) lvar op.
+Defined.
Instance reify_one (R:Type) lvar op
`{Ring (T:=R)(ring1:=op)}
: reify (ring1:=op) (PEc 1%Z) lvar op.
+Defined.
Instance reifyZ0 (R:Type) lvar
`{Ring (T:=R)}
: reify (PEc Z0) lvar Z0|11.
+Defined.
Instance reifyZpos (R:Type) lvar (p:positive)
`{Ring (T:=R)}
: reify (PEc (Zpos p)) lvar (Zpos p)|11.
+Defined.
Instance reifyZneg (R:Type) lvar (p:positive)
`{Ring (T:=R)}
: reify (PEc (Zneg p)) lvar (Zneg p)|11.
+Defined.
Instance reify_add (R:Type)
e1 lvar t1 e2 t2 op
@@ -69,6 +78,7 @@ Instance reify_add (R:Type)
{_:reify (add:=op) e1 lvar t1}
{_:reify (add:=op) e2 lvar t2}
: reify (add:=op) (PEadd e1 e2) lvar (op t1 t2).
+Defined.
Instance reify_mul (R:Type)
e1 lvar t1 e2 t2 op
@@ -76,6 +86,7 @@ Instance reify_mul (R:Type)
{_:reify (mul:=op) e1 lvar t1}
{_:reify (mul:=op) e2 lvar t2}
: reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2)|10.
+Defined.
Instance reify_mul_ext (R:Type) `{Ring R}
lvar (z:Z) e2 t2
@@ -83,6 +94,7 @@ Instance reify_mul_ext (R:Type) `{Ring R}
{_:reify e2 lvar t2}
: reify (PEmul (PEc z) e2) lvar
(@multiplication Z _ _ z t2)|9.
+Defined.
Instance reify_sub (R:Type)
e1 lvar t1 e2 t2 op
@@ -90,24 +102,28 @@ Instance reify_sub (R:Type)
{_:reify (sub:=op) e1 lvar t1}
{_:reify (sub:=op) e2 lvar t2}
: reify (sub:=op) (PEsub e1 e2) lvar (op t1 t2).
+Defined.
Instance reify_opp (R:Type)
e1 lvar t1 op
`{Ring (T:=R)(opp:=op)}
{_:reify (opp:=op) e1 lvar t1}
: reify (opp:=op) (PEopp e1) lvar (op t1).
+Defined.
Instance reify_pow (R:Type) `{Ring R}
e1 lvar t1 n
`{Ring (T:=R)}
{_:reify e1 lvar t1}
: reify (PEpow e1 n) lvar (pow_N t1 n)|1.
+Defined.
Instance reify_var (R:Type) t lvar i
`{nth R t lvar i}
`{Rr: Ring (T:=R)}
: reify (Rr:= Rr) (PEX Z (Pos.of_succ_nat i))lvar t
| 100.
+Defined.
Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R)
(lterm:list R).
@@ -115,12 +131,14 @@ Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R)
Instance reify_nil (R:Type) lvar
`{Rr: Ring (T:=R)}
: reifylist (Rr:= Rr) nil lvar (@nil R).
+Defined.
Instance reify_cons (R:Type) e1 lvar t1 lexpr2 lterm2
`{Rr: Ring (T:=R)}
{_:reify (Rr:= Rr) e1 lvar t1}
{_:reifylist (Rr:= Rr) lexpr2 lvar lterm2}
: reifylist (Rr:= Rr) (e1::lexpr2) lvar (t1::lterm2).
+Defined.
Definition list_reifyl (R:Type) lexpr lvar lterm
`{Rr: Ring (T:=R)}
diff --git a/plugins/setoid_ring/Rings_Q.v b/plugins/setoid_ring/Rings_Q.v
index ae91ee1664..df3677e1c3 100644
--- a/plugins/setoid_ring/Rings_Q.v
+++ b/plugins/setoid_ring/Rings_Q.v
@@ -15,6 +15,7 @@ Require Export Integral_domain.
Require Import QArith.
Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq).
+Defined.
Instance Qri : (Ring (Ro:=Qops)).
constructor.
diff --git a/plugins/setoid_ring/Rings_R.v b/plugins/setoid_ring/Rings_R.v
index 901b36ed3b..fe7558845d 100644
--- a/plugins/setoid_ring/Rings_R.v
+++ b/plugins/setoid_ring/Rings_R.v
@@ -20,6 +20,7 @@ constructor;red;intros;subst;trivial.
Qed.
Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)).
+Defined.
Instance Rri : (Ring (Ro:=Rops)).
constructor;
diff --git a/test-suite/bugs/closed/HoTT_coq_056.v b/test-suite/bugs/closed/HoTT_coq_056.v
index 3e3a987a7c..b80e0bb0e4 100644
--- a/test-suite/bugs/closed/HoTT_coq_056.v
+++ b/test-suite/bugs/closed/HoTT_coq_056.v
@@ -94,9 +94,9 @@ Definition FunctorApplicationOf {C D} F {argsT} args {T} {rtn}
Global Arguments FunctorApplicationOf / {C} {D} F {argsT} args {T} {rtn} {_}.
Global Instance FunctorApplicationDash C D (F : Functor C D)
-: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0.
+: FunctorApplicationInterpretable F (IdentityFunctor C) F | 0 := {}.
Global Instance FunctorApplicationFunctorFunctor' A B C C' D (F : Functor (A * B) D) (G : Functor C A) (H : Functor C' B)
-: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100.
+: FunctorApplicationInterpretable F (G, H) (F ∘ (FunctorProduct' G H))%functor | 100 := {}.
Notation "F ⟨ x ⟩" := (FunctorApplicationOf F%functor x%functor) : functor_scope.
diff --git a/test-suite/bugs/closed/bug_3324.v b/test-suite/bugs/closed/bug_3324.v
index 45dbb57aa2..dae0d4c024 100644
--- a/test-suite/bugs/closed/bug_3324.v
+++ b/test-suite/bugs/closed/bug_3324.v
@@ -6,7 +6,7 @@ Module ETassi.
Record hProp := hp { hproptype :> Type ; isp : IsHProp hproptype}.
Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
- Global Instance isset_hProp : IsHSet hProp | 0.
+ Global Instance isset_hProp : IsHSet hProp | 0 := {}.
Check (eq_refl _ : setT (default_HSet _ _) = hProp).
Check (eq_refl _ : setT _ = hProp).
@@ -22,7 +22,7 @@ Module JGross.
Definition Unit_hp:hProp:=(hp Unit admit).
Record hSet := BuildhSet {setT:> Type; iss :> IsHSet setT}.
Canonical Structure default_HSet:= fun T P => (@BuildhSet T P).
- Global Instance isset_hProp : IsHSet hProp | 0.
+ Global Instance isset_hProp : IsHSet hProp | 0 := {}.
Definition isepi {X Y} `(f:X->Y) := forall Z: hSet,
forall g h: Y -> Z, (fun x => g (f x)) = (fun x => h (f x)) -> g = h.
Lemma isepi_issurj {X Y} (f:X->Y): isepi f -> True.
diff --git a/test-suite/bugs/closed/bug_3454.v b/test-suite/bugs/closed/bug_3454.v
index e4cd60cb24..0a01adec33 100644
--- a/test-suite/bugs/closed/bug_3454.v
+++ b/test-suite/bugs/closed/bug_3454.v
@@ -32,14 +32,14 @@ Local Instance isequiv_tgt_compose A B
: @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
(A -> B)
(@compose A {xy : B * B & fst xy = snd xy} B
- (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)).
+ (@compose {xy : B * B & fst xy = snd xy} _ B (@snd B B) pr1)) := {}.
(* Toplevel input, characters 220-223: *)
(* Error: Cannot infer this placeholder. *)
Local Instance isequiv_tgt_compose' A B
: @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
(A -> B)
- (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)).
+ (@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _) pr1)) := {}.
(* Toplevel input, characters 221-232: *)
(* Error: *)
(* In environment *)
@@ -52,7 +52,7 @@ Local Instance isequiv_tgt_compose'' A B
: @IsEquiv (A -> {xy : B * B & fst xy = snd xy})
(A -> B)
(@compose A {xy : B * B & fst xy = snd xy} B (@compose {xy : B * B & fst xy = snd xy} _ B (@snd _ _)
- (fun s => s.(projT1)))).
+ (fun s => s.(projT1)))) := {}.
(* Toplevel input, characters 15-241:
Error:
Cannot infer an internal placeholder of type "Type" in environment:
diff --git a/test-suite/bugs/closed/bug_3682.v b/test-suite/bugs/closed/bug_3682.v
index 9d37d1a2d0..07b759afb5 100644
--- a/test-suite/bugs/closed/bug_3682.v
+++ b/test-suite/bugs/closed/bug_3682.v
@@ -1,6 +1,6 @@
Require Import TestSuite.admit.
Class Foo.
Definition bar `{Foo} (x : Set) := Set.
-Instance: Foo.
+Instance: Foo := {}.
Definition bar1 := bar nat.
Definition bar2 := bar ltac:(admit).
diff --git a/test-suite/bugs/closed/bug_4782.v b/test-suite/bugs/closed/bug_4782.v
index be17a96f15..c08195d502 100644
--- a/test-suite/bugs/closed/bug_4782.v
+++ b/test-suite/bugs/closed/bug_4782.v
@@ -15,8 +15,8 @@ Record T := { dom : Type }.
Definition pairT A B := {| dom := (dom A * dom B)%type |}.
Class C (A:Type).
Parameter B:T.
-Instance c (A:T) : C (dom A).
-Instance cn : C (dom B).
+Instance c (A:T) : C (dom A) := {}.
+Instance cn : C (dom B) := {}.
Parameter F : forall A:T, C (dom A) -> forall x:dom A, x=x -> A = A.
Set Typeclasses Debug.
Goal forall (A:T) (x:dom A), pairT A A = pairT A A.
diff --git a/test-suite/bugs/closed/bug_5401.v b/test-suite/bugs/closed/bug_5401.v
index 95193b993b..466e669d00 100644
--- a/test-suite/bugs/closed/bug_5401.v
+++ b/test-suite/bugs/closed/bug_5401.v
@@ -5,7 +5,7 @@ Parameter P : nat -> Type.
Parameter v : forall m, P m.
Parameter f : forall (P : nat -> Type), (forall a, P a) -> P 0.
Class U (R : P 0) (m : forall x, P x) : Prop.
-Instance w : U (f _ (fun _ => v _)) v.
+Instance w : U (f _ (fun _ => v _)) v := {}.
Print HintDb typeclass_instances.
End A.
diff --git a/test-suite/success/Typeclasses.v b/test-suite/success/Typeclasses.v
index 9086621344..3888cafed3 100644
--- a/test-suite/success/Typeclasses.v
+++ b/test-suite/success/Typeclasses.v
@@ -14,7 +14,7 @@ Module onlyclasses.
Module RJung.
Class Foo (x : nat).
- Instance foo x : x = 2 -> Foo x.
+ Instance foo x : x = 2 -> Foo x := {}.
Hint Extern 0 (_ = _) => reflexivity : typeclass_instances.
Typeclasses eauto := debug.
Check (_ : Foo 2).
@@ -63,7 +63,7 @@ End RefineVsNoTceauto.
Module Leivantex2PR339.
(** Was a bug preventing to find hints associated with no pattern *)
Class Bar := {}.
- Instance bar1 (t:Type) : Bar.
+ Instance bar1 (t:Type) : Bar := {}.
Hint Extern 0 => exact True : typeclass_instances.
Typeclasses eauto := debug.
Goal Bar.
@@ -222,10 +222,10 @@ Module IterativeDeepening.
Class B.
Class C.
- Instance: B -> A | 0.
- Instance: C -> A | 0.
- Instance: C -> B -> A | 0.
- Instance: A -> A | 0.
+ Instance: B -> A | 0 := {}.
+ Instance: C -> A | 0 := {}.
+ Instance: C -> B -> A | 0 := {}.
+ Instance: A -> A | 0 := {}.
Goal C -> A.
intros.
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index 5477c83316..62a66daf7d 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -51,7 +51,7 @@ Qed.
Class B (A : Type).
Class I.
-Instance i : I.
+Instance i : I := {}.
Definition flip {A B C : Type} (f : A -> B -> C) := fun y x => f x y.
Class D (f : nat -> nat -> nat).
@@ -59,7 +59,7 @@ Definition ftest (x y : nat) := x + y.
Definition flipD (f : nat -> nat -> nat) : D f -> D (flip f).
Admitted.
Module Instnopat.
- Local Instance: B nat.
+ Local Instance: B nat := {}.
(* pattern_of_constr -> B nat *)
(* exact hint *)
Check (_ : B nat).
@@ -72,7 +72,7 @@ Module Instnopat.
eauto with typeclass_instances.
Qed.
- Local Instance: D ftest.
+ Local Instance: D ftest := {}.
Local Hint Resolve flipD | 0 : typeclass_instances.
(* pattern: D (flip _) *)
Fail Timeout 1 Check (_ : D _). (* loops applying flipD *)
@@ -80,7 +80,7 @@ Module Instnopat.
End Instnopat.
Module InstnopatApply.
- Local Instance: I -> B nat.
+ Local Instance: I -> B nat := {}.
(* pattern_of_constr -> B nat *)
(* apply hint *)
Check (_ : B nat).
@@ -116,7 +116,7 @@ Module InstPat.
Hint Extern 0 (D (flip _)) => apply flipD : typeclass_instances.
Module withftest.
- Local Instance: D ftest.
+ Local Instance: D ftest := {}.
Check (_ : D _).
(* D_instance_0 : D ftest *)
diff --git a/test-suite/success/bteauto.v b/test-suite/success/bteauto.v
index 730b367d60..cea7d92c0b 100644
--- a/test-suite/success/bteauto.v
+++ b/test-suite/success/bteauto.v
@@ -149,10 +149,10 @@ Module IterativeDeepening.
Class B.
Class C.
- Instance: B -> A | 0.
- Instance: C -> A | 0.
- Instance: C -> B -> A | 0.
- Instance: A -> A | 0.
+ Instance: B -> A | 0 := {}.
+ Instance: C -> A | 0 := {}.
+ Instance: C -> B -> A | 0 := {}.
+ Instance: A -> A | 0 := {}.
Goal C -> A.
intros.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index d1d384659b..573912c7cd 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -263,7 +263,7 @@ Abort.
(* This one was working in 8.4 (because of full conv on closed arguments) *)
Class E.
-Instance a:E.
+Instance a:E := {}.
Goal forall h : E -> nat -> nat, h (id a) 0 = h a 0.
intros.
destruct (h _).
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index c44747379f..5b616ccc33 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -9,11 +9,11 @@
(************************************************************************)
Class A (A : Type).
- Instance an: A nat.
+ Instance an: A nat := {}.
Class B (A : Type) (a : A).
-Instance bn0: B nat 0.
-Instance bn1: B nat 1.
+Instance bn0: B nat 0 := {}.
+Instance bn1: B nat 1 := {}.
Goal A nat.
Proof.
@@ -39,7 +39,7 @@ Proof.
eexists. eexists. typeclasses eauto.
Defined.
-Instance ab: A bool. (* Backtrack on A instance *)
+Instance ab: A bool := {}. (* Backtrack on A instance *)
Goal exists (T : Type) (t : T), A T /\ B T t.
Proof.
eexists. eexists. typeclasses eauto.
@@ -51,7 +51,7 @@ Hint Extern 0 { x : ?A & _ } =>
unshelve class_apply @existT : typeclass_instances.
Existing Class sigT.
Set Typeclasses Debug.
-Instance can: C an 0.
+Instance can: C an 0 := {}.
(* Backtrack on instance implementation *)
Goal exists (T : Type) (t : T), { x : A T & C x t }.
Proof.
@@ -59,7 +59,7 @@ Proof.
Defined.
Class D T `(a: A T).
- Instance: D _ an.
+ Instance: D _ an := {}.
Goal exists (T : Type), { x : A T & D T x }.
Proof.
eexists. typeclasses eauto.
diff --git a/test-suite/success/setoid_test2.v b/test-suite/success/setoid_test2.v
index 79467e549c..351481b0b6 100644
--- a/test-suite/success/setoid_test2.v
+++ b/test-suite/success/setoid_test2.v
@@ -120,7 +120,7 @@ Axiom eqS1: S1 -> S1 -> Prop.
Axiom SetoidS1 : Setoid_Theory S1 eqS1.
Add Setoid S1 eqS1 SetoidS1 as S1setoid.
-Instance eqS1_default : DefaultRelation eqS1.
+Instance eqS1_default : DefaultRelation eqS1 := {}.
Axiom eqS1': S1 -> S1 -> Prop.
Axiom SetoidS1' : Setoid_Theory S1 eqS1'.
@@ -220,7 +220,7 @@ Axiom eqS1_test8: S1_test8 -> S1_test8 -> Prop.
Axiom SetoidS1_test8 : Setoid_Theory S1_test8 eqS1_test8.
Add Setoid S1_test8 eqS1_test8 SetoidS1_test8 as S1_test8setoid.
-Instance eqS1_test8_default : DefaultRelation eqS1_test8.
+Instance eqS1_test8_default : DefaultRelation eqS1_test8 := {}.
Axiom f_test8 : S2 -> S1_test8.
Add Morphism f_test8 with signature (eqS2 ==> eqS1_test8) as f_compat_test8. Admitted.
diff --git a/theories/Classes/CRelationClasses.v b/theories/Classes/CRelationClasses.v
index bc821532fe..bb873588b1 100644
--- a/theories/Classes/CRelationClasses.v
+++ b/theories/Classes/CRelationClasses.v
@@ -177,6 +177,7 @@ Section Defs.
a rewrite crelation. *)
Global Instance equivalence_rewrite_crelation `(Equivalence eqA) : RewriteRelation eqA.
+ Defined.
(** Leibniz equality. *)
Section Leibniz.
@@ -195,7 +196,10 @@ End Defs.
(** Default rewrite crelations handled by [setoid_rewrite]. *)
Instance: RewriteRelation impl.
+Defined.
+
Instance: RewriteRelation iff.
+Defined.
(** Hints to drive the typeclass resolution avoiding loops
due to the use of full unification. *)
@@ -299,7 +303,8 @@ Section Binary.
fun R R' => forall x y, iffT (R x y) (R' x y).
Global Instance: RewriteRelation relation_equivalence.
-
+ Defined.
+
Definition relation_conjunction (R : crelation A) (R' : crelation A) : crelation A :=
fun x y => prod (R x y) (R' x y).
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 4b97d75cea..6e2ff49536 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -171,6 +171,7 @@ Section Defs.
a rewrite relation. *)
Global Instance equivalence_rewrite_relation `(Equivalence eqA) : RewriteRelation eqA.
+ Defined.
(** Leibniz equality. *)
Section Leibniz.
@@ -189,7 +190,9 @@ End Defs.
(** Default rewrite relations handled by [setoid_rewrite]. *)
Instance: RewriteRelation impl.
+Defined.
Instance: RewriteRelation iff.
+Defined.
(** Hints to drive the typeclass resolution avoiding loops
due to the use of full unification. *)
@@ -430,6 +433,7 @@ Section Binary.
@predicate_equivalence (_::_::Tnil).
Global Instance: RewriteRelation relation_equivalence.
+ Defined.
Definition relation_conjunction (R : relation A) (R' : relation A) : relation A :=
@predicate_intersection (A::A::Tnil) R R'.
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index 3e6358c8f3..341dacd4b2 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -62,7 +62,10 @@ Class Measure {A B} (f : A -> B).
(** Standard measures. *)
Instance fst_measure : @Measure (A * B) A Fst.
+Defined.
+
Instance snd_measure : @Measure (A * B) B Snd.
+Defined.
(** We define a product relation over [A*B]: each components should
satisfy the corresponding initial relation. *)
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 3fab3c5a07..94920f74ec 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -41,6 +41,7 @@ Definition default_relation `{DefaultRelation A R} := R.
(lowest priority). *)
Instance equivalence_default `(Equivalence A R) : DefaultRelation R | 4.
+Defined.
(** The setoid_replace tactics in Ltac, defined in terms of default relations
and the setoid_rewrite tactic. *)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 748a2628c5..5cac6af4b2 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -269,9 +269,9 @@ let do_instance env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode ct
Pretyping.check_evars env (Evd.from_env env) sigma termtype;
let termtype = to_constr sigma termtype in
let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
- if not (Evd.has_undefined sigma) && not (Option.is_empty term) then
+ if not (Evd.has_undefined sigma) && not (Option.is_empty props) then
declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype
- else if program_mode || refine || Option.is_empty term then
+ else if program_mode || refine || Option.is_empty props then
declare_instance_open env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype
else CErrors.user_err Pp.(str "Unsolved obligations remaining.");
id
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:23:43 +0000