aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/3368.v
diff options
context:
space:
mode:
authorVincent Laporte2018-10-02 13:44:46 +0000
committerVincent Laporte2018-10-04 08:01:34 +0000
commitdb22ae6140259dd065fdd80af4cb3c3bab41c184 (patch)
treee17ad7016014a4e2dd4001d826575342c2812fc3 /test-suite/bugs/closed/3368.v
parent53929e9bacf251f60c85d4ff24d46fec2c42ab4b (diff)
rename test files (do not start by a digit)
Diffstat (limited to 'test-suite/bugs/closed/3368.v')
-rw-r--r--test-suite/bugs/closed/3368.v16
1 files changed, 0 insertions, 16 deletions
diff --git a/test-suite/bugs/closed/3368.v b/test-suite/bugs/closed/3368.v
deleted file mode 100644
index 1eff1dba8a..0000000000
--- a/test-suite/bugs/closed/3368.v
+++ /dev/null
@@ -1,16 +0,0 @@
-(* 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. *)