blob: 09bd789345780dd8310a2e9060895902783372b8 (
plain)
1
2
3
4
|
(* -*- mode: coq; coq-prog-args: ("-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.
|
