diff options
| -rw-r--r-- | test-suite/bugs/closed/3368.v (renamed from test-suite/bugs/opened/3368.v) | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/opened/3368.v b/test-suite/bugs/closed/3368.v index c0c00b4ed..64fb03568 100644 --- a/test-suite/bugs/opened/3368.v +++ b/test-suite/bugs/closed/3368.v @@ -6,10 +6,10 @@ 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). -Fail Definition opposite' C D (F : Functor C D) +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 s d). + (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. *) |