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:28 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2019-02-02 19:29:28 -0500
commit1ef7f1c0c6897535a86daa77799714e25638f5e9 (patch)
tree5bcca733632ecc84d2c6b1ee48cb2e557a7adba5 /dev/build/windows/patches_coq/aactactis-86ac28259030649ef51460e4de2441c8a1017751.patch
parent3a2fac7bcee36fd9dcb4f39a615c8ac0349abcc9 (diff)
parent9ebf44d84754adc5b64fcf612c6816c02c80462d (diff)
Updated version 8.9.0 from 'upstream/8.9.0'
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