diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-07-15 13:15:50 +0200 |
| commit | e347929583f820a2cc0296597b6382309e930989 (patch) | |
| tree | cdc3f18fc5c66a9d3d7cc8404c6a295169e41fcc /test-suite/bugs/closed/HoTT_coq_107.v | |
| parent | c01be74d81a5466c58f8dc6c568db286b0979997 (diff) | |
| parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) | |
Merge tag 'upstream/8.5_beta2+dfsg' into test
Upstream version 8.5~beta2+dfsg
Diffstat (limited to 'test-suite/bugs/closed/HoTT_coq_107.v')
| -rw-r--r-- | test-suite/bugs/closed/HoTT_coq_107.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test-suite/bugs/closed/HoTT_coq_107.v b/test-suite/bugs/closed/HoTT_coq_107.v index c3a83627..7c1ab8dc 100644 --- a/test-suite/bugs/closed/HoTT_coq_107.v +++ b/test-suite/bugs/closed/HoTT_coq_107.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-nois" "-emacs") -*- *) +(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-R" "../theories" "Coq") -*- *) (* File reduced by coq-bug-finder from 4897 lines to 2605 lines, then from 2297 lines to 236 lines, then from 239 lines to 137 lines, then from 118 lines to 67 lines, then from 520 lines to 76 lines. *) (** Note: The bug here is the same as the #113, that is, HoTT_coq_113.v *) Require Import Coq.Init.Logic. @@ -59,7 +59,7 @@ Instance trunc_sigma `{P : A -> Type} Proof. generalize dependent A. - induction n; [ | admit ]; simpl; intros A P ac Pc. + induction n; [ | apply admit ]; simpl; intros A P ac Pc. (exists (existT _ (center A) (center (P (center A))))). intros [a ?]. refine (path_sigma' P (contr a) (path_contr _ _)). @@ -102,5 +102,5 @@ The term | false => B end))" (Universe inconsistency: Cannot enforce Top.197 = Set)). *) - admit. + apply admit. Defined. |