diff options
Diffstat (limited to 'test-suite/bugs/closed/3352.v')
| -rw-r--r-- | test-suite/bugs/closed/3352.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/bugs/closed/3352.v b/test-suite/bugs/closed/3352.v index f8113e4c..bf2f7a9d 100644 --- a/test-suite/bugs/closed/3352.v +++ b/test-suite/bugs/closed/3352.v @@ -20,7 +20,7 @@ while it is expected to have type "IsHProp (* Top.17 *) Empty" Defined. Module B. -(* -*- coq-prog-args: ("-emacs" "-indices-matter") -*- *) +(* -*- coq-prog-args: ("-indices-matter") -*- *) (* File reduced by coq-bug-finder from original input, then from 7725 lines to 78 lines, then from 51 lines to 13 lines *) Set Universe Polymorphism. Inductive paths {A} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. @@ -32,4 +32,4 @@ simpl. Set Printing Universes. exact hprop_Empty. Defined. -End B.
\ No newline at end of file +End B. |