summaryrefslogtreecommitdiff
path: root/dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:23 -0500
commit9ebf44d84754adc5b64fcf612c6816c02c80462d (patch)
treebf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch
parent9043add656177eeac1491a73d2f3ab92bec0013c (diff)
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch')
-rw-r--r--dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch21
1 files changed, 0 insertions, 21 deletions
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