Mercurial > cpdt > repo

diff src/MoreDep.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 a0b8b550e265
children 4a57a4922af5
line wrap: on
line diff
--- a/src/MoreDep.v	Tue Oct 07 10:43:54 2008 -0400
+++ b/src/MoreDep.v	Tue Oct 07 10:49:07 2008 -0400
@@ -349,7 +349,7 @@
 Require Import Ascii String.
 Open Scope string_scope.
 
-Inductive regexp : (string -> Prop) -> Set :=
+Inductive regexp : (string -> Prop) -> Type :=
 | Char : forall ch : ascii,
   regexp (fun s => s = String ch "")
 | Concat : forall P1 P2 (r1 : regexp P1) (r2 : regexp P2),