diff options
Diffstat (limited to 'dev/build/windows/patches_coq')
| -rwxr-xr-x | dev/build/windows/patches_coq/VST.patch | 15 | ||||
| -rw-r--r-- | dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch | 21 | ||||
| -rwxr-xr-x[-rw-r--r--] | dev/build/windows/patches_coq/quickchick.patch (renamed from dev/build/windows/patches_coq/quickchick-v1.0.2.patch) | 12 |
3 files changed, 15 insertions, 33 deletions
diff --git a/dev/build/windows/patches_coq/VST.patch b/dev/build/windows/patches_coq/VST.patch new file mode 100755 index 00000000..2c8c4637 --- /dev/null +++ b/dev/build/windows/patches_coq/VST.patch @@ -0,0 +1,15 @@ +diff --git a/Makefile b/Makefile +index 4a119042..fdfac13e 100755 +--- a/Makefile ++++ b/Makefile +@@ -76,8 +76,8 @@ endif + + COMPCERTDIRS=lib common $(ARCHDIRS) cfrontend flocq exportclight $(BACKEND) + +-COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) compcert.$(d)) +-EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) compcert.$(d)) ++COMPCERT_R_FLAGS= $(foreach d, $(COMPCERTDIRS), -R $(COMPCERT)/$(d) VST.compcert.$(d)) ++EXTFLAGS= $(foreach d, $(COMPCERTDIRS), -Q $(COMPCERT)/$(d) VST.compcert.$(d)) + + # for SSReflect + ifdef MATHCOMP diff --git a/dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch b/dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch deleted file mode 100644 index d9b134b2..00000000 --- a/dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch +++ /dev/null @@ -1,21 +0,0 @@ ---- aac-tactics-v8.8.orig\Tutorial.v 2018-05-30 16:09:06.000000000 +0200 -+++ aac-tactics-v8.8\Tutorial.v 2018-08-24 19:47:25.000000000 +0200 -@@ -9,16 +9,14 @@ - (** * Tutorial for using the [aac_tactics] library. - - Depending on your installation, either modify the following two - lines, or add them to your .coqrc files, replacing "." with the - path to the [aac_tactics] library. *) - --Add Rec LoadPath "." as AAC_tactics. --Add ML Path ".". --Require Import AAC. --Require Instances. -+Require Import AAC_tactics.AAC. -+Require AAC_tactics.Instances. - Require Arith ZArith. - - (** ** Introductory example - - Here is a first example with relative numbers ([Z]): one can - rewrite an universally quantified hypothesis modulo the diff --git a/dev/build/windows/patches_coq/quickchick-v1.0.2.patch b/dev/build/windows/patches_coq/quickchick.patch index d03749ba..1afa6e7f 100644..100755 --- a/dev/build/windows/patches_coq/quickchick-v1.0.2.patch +++ b/dev/build/windows/patches_coq/quickchick.patch @@ -24,15 +24,3 @@ ORIGFOLDER= quickchick-v1.0.2.orig + $(V)cp $(QCTOOL_EXE) "$(COQBIN)/quickChick" # $(V)cp src/quickChickLib.cmx $(COQLIB)/user-contrib/QuickChick # $(V)cp src/quickChickLib.o $(COQLIB)/user-contrib/QuickChick - ---- quickchick-v1.0.2.orig/src/Show.v 2018-08-22 18:21:39.000000000 +0200 -+++ quickchick-v1.0.2/src/Show.v 2018-08-27 09:21:35.893961900 +0200 -@@ -228,7 +228,7 @@ - match s with - | EmptyString => (if b then ")" else "", b) - | String a s => -- let (s', b) := aux s (orb b (nat_of_ascii a =? 32)) in -+ let (s', b) := aux s (orb b (nat_of_ascii a =? 32)%nat) in - (String a s', b) - end in - let (s', b) := aux s false in |