diff options
Diffstat (limited to 'test-suite/bugs/closed/3023.v')
-rw-r--r-- | test-suite/bugs/closed/3023.v | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/3023.v b/test-suite/bugs/closed/3023.v new file mode 100644 index 00000000..ed489511 --- /dev/null +++ b/test-suite/bugs/closed/3023.v @@ -0,0 +1,31 @@ +(* Checking use of eta on Flexible/Rigid and SemiFlexible/Rigid unif problems *) + +Set Implicit Arguments. +Generalizable All Variables. + +Record Category {obj : Type} := + { + Morphism : obj -> obj -> Type; + + Identity : forall x, Morphism x x; + Compose : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'; + LeftIdentity : forall a b (f : Morphism a b), Compose (Identity b) f = f + }. + + +Section DiscreteAdjoints. + Let C := {| + Morphism := (fun X Y : Type => X -> Y); + Identity := (fun X : Type => (fun x : X => x)); + Compose := (fun _ _ _ f g => (fun x => f (g x))); + LeftIdentity := (fun X Y p => @eq_refl _ p : (fun x : X => p x) = p) + |}. + Variable ObjectFunctor : C = C. + + Goal True. + Proof. + subst C. + revert ObjectFunctor. + intro ObjectFunctor. + simpl in ObjectFunctor. + revert ObjectFunctor. (* Used to failed in 8.4 up to 16 April 2013 *) |