diff options
Diffstat (limited to 'test-suite/bugs/closed/3612.v')
| -rw-r--r-- | test-suite/bugs/closed/3612.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v index a5476850..33e5d532 100644 --- a/test-suite/bugs/closed/3612.v +++ b/test-suite/bugs/closed/3612.v @@ -1,4 +1,4 @@ -(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter" "-nois") -*- *) +(* -*- mode: coq; coq-prog-args: ("-indices-matter" "-nois") -*- *) (* File reduced by coq-bug-finder from original input, then from 3595 lines to 3518 lines, then from 3133 lines to 2950 lines, then from 2911 lines to 415 lines, then from 431 lines to 407 \ lines, then from 421 lines to 428 lines, then from 444 lines to 429 lines, then from 434 lines to 66 lines, then from 163 lines to 48 lines *) (* coqc version trunk (September 2014) compiled on Sep 11 2014 14:48:8 with OCaml 4.01.0 @@ -38,7 +38,9 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P) (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2), p = q. -Declare ML Module "coretactics". +Declare ML Module "ltac_plugin". + +Set Default Proof Mode "Classic". Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x)) (xx : @paths (@sigT A (fun x0 : A => B x0)) x x), |