changeset 89:939add5a7db9

Remove -impredicative-set
author Adam Chlipala <adamc@hcoop.net>
date Tue, 07 Oct 2008 10:49:07 -0400
parents cde1351d18bb
children 9b0d118abbc9
files Makefile src/MoreDep.v src/MoreSpecif.v src/Subset.v
diffstat 4 files changed, 5 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/Makefile	Tue Oct 07 10:43:54 2008 -0400
+++ b/Makefile	Tue Oct 07 10:49:07 2008 -0400
@@ -15,8 +15,8 @@
 
 Makefile.coq: Makefile $(VS)
 	coq_makefile $(VS) \
-		COQC = "coqc -I src -impredicative-set \
-			-dump-glob $(GLOBALS)" \
+		COQC = "coqc -I src -dump-glob $(GLOBALS)" \
+		COQDEP = "coqdep -I src" \
 		-o Makefile.coq
 
 clean:: Makefile.coq
--- 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),
--- 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.
 
--- a/src/Subset.v	Tue Oct 07 10:43:54 2008 -0400
+++ b/src/Subset.v	Tue Oct 07 10:49:07 2008 -0400
@@ -428,7 +428,7 @@
 
 (** Our final implementation of dependent predecessor used a very specific argument type to ensure that execution could always complete normally.  Sometimes we want to allow execution to fail, and we want a more principled way of signaling that than returning a default value, as [pred] does for [0].  One approach is to define this type family [maybe], which is a version of [sig] that allows obligation-free failure. *)
 
-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.