From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- test-suite/bugs/closed/3368.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 test-suite/bugs/closed/3368.v (limited to 'test-suite/bugs/closed/3368.v') diff --git a/test-suite/bugs/closed/3368.v b/test-suite/bugs/closed/3368.v new file mode 100644 index 00000000..1eff1dba --- /dev/null +++ b/test-suite/bugs/closed/3368.v @@ -0,0 +1,16 @@ +(* File reduced by coq-bug-finder from 7411 lines to 2271 lines., then from 889 lines to 119 lines, then from 76 lines to 19 lines *) +Set Universe Polymorphism. +Set Implicit Arguments. +Set Primitive Projections. +Record PreCategory := { object :> Type; morphism : object -> object -> Type }. +Record Functor (C D : PreCategory) := + { object_of :> C -> D; + morphism_of : forall s d, morphism C s d -> morphism D (object_of s) (object_of d) }. +Definition opposite (C : PreCategory) : PreCategory := @Build_PreCategory C (fun s d => morphism C d s). +Definition opposite' C D (F : Functor C D) + := Build_Functor (opposite C) (opposite D) + (object_of F) + (fun s d => @morphism_of C D F d s). +(* Toplevel input, characters 15-191: +Anomaly: File "pretyping/reductionops.ml", line 149, characters 4-10: Assertion failed. +Please report. *) -- cgit v1.2.3