Merge PR #984: Handling primitive projections in canonical structures.

1 files changed, 52 insertions, 2 deletions

diff --git a/test-suite/bugs/closed/5692.v b/test-suite/bugs/closed/5692.v
index 55ef7abe40..4c8d464f19 100644
--- a/test-suite/bugs/closed/5692.v
+++ b/test-suite/bugs/closed/5692.v
@@ -1,9 +1,59 @@
 Set Primitive Projections.
 Require Import ZArith ssreflect.
 
-Module Test3.
+Module Test1.
 
-Set Primitive Projections.
+Structure semigroup := SemiGroup {
+  sg_car :> Type;
+  sg_op : sg_car -> sg_car -> sg_car;
+}.
+
+Structure monoid := Monoid {
+  monoid_car :> Type;
+  monoid_op : monoid_car -> monoid_car -> monoid_car;
+  monoid_unit : monoid_car;
+}.
+
+Coercion monoid_sg (X : monoid) : semigroup :=
+  SemiGroup (monoid_car X) (monoid_op X).
+Canonical Structure monoid_sg.
+
+Parameter X : monoid.
+Parameter x y : X.
+
+Check (sg_op _ x y).
+
+End Test1.
+
+Module Test2.
+
+Structure semigroup := SemiGroup {
+  sg_car :> Type;
+  sg_op : sg_car -> sg_car -> sg_car;
+}.
+
+Structure monoid := Monoid {
+  monoid_car :> Type;
+  monoid_op : monoid_car -> monoid_car -> monoid_car;
+  monoid_unit : monoid_car;
+  monoid_left_id x : monoid_op monoid_unit x = x;
+}.
+
+Coercion monoid_sg (X : monoid) : semigroup :=
+  SemiGroup (monoid_car X) (monoid_op X).
+Canonical Structure monoid_sg.
+
+Canonical Structure nat_sg := SemiGroup nat plus.
+Canonical Structure nat_monoid := Monoid nat plus 0 plus_O_n.
+
+Lemma foo (x : nat) : 0 + x = x.
+Proof.
+apply monoid_left_id.
+Qed.
+
+End Test2.
+
+Module Test3.
 
 Structure semigroup := SemiGroup {
   sg_car :> Type;