Remove -impredicative-set

Makefile

@@ -15,8 +15,8 @@ coq: Makefile.coq
 
 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

src/MoreDep.v

@@ -349,7 +349,7 @@ Qed.
 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),

src/MoreSpecif.v

@@ -45,7 +45,7 @@ End sumbool_and.
 
 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.
 

src/Subset.v

@@ -428,7 +428,7 @@ let rec in_dec a_eq_dec x = function
 
 (** 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.