diff options
| author | Vincent Laporte | 2018-10-02 13:44:46 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-10-04 08:01:34 +0000 |
| commit | db22ae6140259dd065fdd80af4cb3c3bab41c184 (patch) | |
| tree | e17ad7016014a4e2dd4001d826575342c2812fc3 /test-suite/bugs/closed/4101.v | |
| parent | 53929e9bacf251f60c85d4ff24d46fec2c42ab4b (diff) | |
rename test files (do not start by a digit)
Diffstat (limited to 'test-suite/bugs/closed/4101.v')
| -rw-r--r-- | test-suite/bugs/closed/4101.v | 19 |
1 files changed, 0 insertions, 19 deletions
diff --git a/test-suite/bugs/closed/4101.v b/test-suite/bugs/closed/4101.v deleted file mode 100644 index 75a26a0670..0000000000 --- a/test-suite/bugs/closed/4101.v +++ /dev/null @@ -1,19 +0,0 @@ -(* File reduced by coq-bug-finder from original input, then from 10940 lines to 152 lines, then from 509 lines to 163 lines, then from 178 lines to 66 lines *) -(* coqc version 8.5beta1 (March 2015) compiled on Mar 2 2015 18:53:10 with OCaml 4.01.0 - coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (e77f178e60918f14eacd1ec0364a491d4cfd0f3f) *) - -Global Set Primitive Projections. -Set Implicit Arguments. -Record sigT {A} (P : A -> Type) := existT { projT1 : A ; projT2 : P projT1 }. -Axiom path_forall : forall {A : Type} {P : A -> Type} (f g : forall x : A, P x), - (forall x, f x = g x) -> f = g. -Lemma sigT_obj_eq -: forall (T : Type) (T0 : T -> Type) - (s s0 : forall s : sigT T0, - sigT (fun _ : T0 (projT1 s) => unit) -> - sigT (fun _ : T0 (projT1 s) => unit)), - s0 = s. -Proof. - intros. - Set Debug Tactic Unification. - apply path_forall. |