blob: 638404f2cb16b1ea8db2871f4ac978ef958c31d9 (
plain)
1
2
3
4
|
(* -*- mode: coq; coq-prog-args: ("-emacs" "-indices-matter") -*- *)
Monomorphic Inductive paths (A : Type) (a : A) : A -> Type := idpath : paths A a a.
(* This should fail with -indices-matter *)
Fail Check paths nat O O : Prop.
|
