# HG changeset patch
# User Adam Chlipala <adamc@hcoop.net>
# Date 1223390947 14400
# Node ID 939add5a7db98ae0817aa761cd551c376cce7082
# Parent  cde1351d18bb8d8b8bcef02a1077494f429ffca6
Remove -impredicative-set

diff -r cde1351d18bb -r 939add5a7db9 Makefile
--- 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
diff -r cde1351d18bb -r 939add5a7db9 src/MoreDep.v
--- 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),
diff -r cde1351d18bb -r 939add5a7db9 src/MoreSpecif.v
--- 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.
 
diff -r cde1351d18bb -r 939add5a7db9 src/Subset.v
--- 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.