Mercurial > cpdt > repo
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.