Mercurial > cpdt > repo

diff src/MoreSpecif.v @ 89:939add5a7db9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Remove -impredicative-set
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Oct 2008 10:49:07 -0400
parents fd505bcb5632
children 6a00d49e85fb
line wrap: on
line diff
--- a/src/MoreSpecif.v	Tue Oct 07 10:43:54 2008 -0400
+++ b/src/MoreSpecif.v	Tue Oct 07 10:49:07 2008 -0400
@@ -45,7 +45,7 @@
 
 Infix "&&" := sumbool_and (at level 40, left associativity) : specif_scope.
 
-Inductive maybe (A : Type) (P : A -> Prop) : Set :=
+Inductive maybe (A : Set) (P : A -> Prop) : Set :=
 | Unknown : maybe P
 | Found : forall x : A, P x -> maybe P.