drop patch restore_g_ssrmatching.mli, refresh some other patches
Ralf Treinen
4 years ago
| 1 | 1 | |
| 2 | 2 | * New upstream pre-release (tagged on github, but not yet officially |
| 3 | 3 | announced). |
| 4 | ||
| 5 | -- Ralf Treinen <treinen@debian.org> Fri, 10 Apr 2020 13:55:46 +0200 | |
| 4 | * Dropped patches: | |
| 5 | - votour-linking (fixed by upstream) | |
| 6 | - restore_g_ssrmatching.mli (fixed by upstream) | |
| 7 | * Refreshed patches: | |
| 8 | - install-coqide-bytecode | |
| 9 | - remove-bytecode-failing-tests.patch | |
| 10 | ||
| 11 | -- Ralf Treinen <treinen@debian.org> Fri, 10 Apr 2020 14:04:23 +0200 | |
| 6 | 12 | |
| 7 | 13 | coq (8.11.0-1) unstable; urgency=medium |
| 8 | 14 |
| 2 | 2 | |
| 3 | 3 | Index: coq/Makefile.ide |
| 4 | 4 | =================================================================== |
| 5 | --- coq.orig/Makefile.ide 2020-01-26 20:04:55.317246792 +0100 | |
| 6 | +++ coq/Makefile.ide 2020-01-26 20:19:35.829561945 +0100 | |
| 7 | @@ -167,8 +167,10 @@ | |
| 5 | --- coq.orig/Makefile.ide 2020-04-10 14:00:08.336620377 +0200 | |
| 6 | +++ coq/Makefile.ide 2020-04-10 14:00:08.316620304 +0200 | |
| 7 | @@ -181,8 +181,10 @@ | |
| 8 | 8 | |
| 9 | 9 | ifeq ($(HASCOQIDE),no) |
| 10 | 10 | install-coqide: install-ide-toploop |
| 18 | 18 | |
| 19 | 19 | Index: coq/test-suite/Makefile |
| 20 | 20 | =================================================================== |
| 21 | --- coq.orig/test-suite/Makefile 2020-01-31 11:53:21.455840571 +0100 | |
| 22 | +++ coq/test-suite/Makefile 2020-01-31 11:53:21.455840571 +0100 | |
| 23 | @@ -109,7 +109,7 @@ | |
| 21 | --- coq.orig/test-suite/Makefile 2020-04-10 14:02:27.557229362 +0200 | |
| 22 | +++ coq/test-suite/Makefile 2020-04-10 14:02:27.557229362 +0200 | |
| 23 | @@ -113,7 +113,7 @@ | |
| 24 | 24 | coqdoc ssr primitive/uint63 primitive/float ltac2 |
| 25 | 25 | |
| 26 | 26 | # All subsystems |
| 0 | Author: Ralf Treinen <treinen@debian.org> | |
| 1 | Description: Restore the file g_ssrmatching.mli from upstream | |
| 2 | ||
| 3 | Index: coq/plugins/ssrmatching/g_ssrmatching.mli | |
| 4 | =================================================================== | |
| 5 | --- /dev/null 1970-01-01 00:00:00.000000000 +0000 | |
| 6 | +++ coq/plugins/ssrmatching/g_ssrmatching.mli 2020-01-31 17:34:28.247712899 +0100 | |
| 7 | @@ -0,0 +1,26 @@ | |
| 8 | +(************************************************************************) | |
| 9 | +(* * The Coq Proof Assistant / The Coq Development Team *) | |
| 10 | +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) | |
| 11 | +(* <O___,, * (see CREDITS file for the list of authors) *) | |
| 12 | +(* \VV/ **************************************************************) | |
| 13 | +(* // * This file is distributed under the terms of the *) | |
| 14 | +(* * GNU Lesser General Public License Version 2.1 *) | |
| 15 | +(* * (see LICENSE file for the text of the license) *) | |
| 16 | +(************************************************************************) | |
| 17 | + | |
| 18 | +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) | |
| 19 | + | |
| 20 | +open Genarg | |
| 21 | +open Ssrmatching | |
| 22 | + | |
| 23 | +(** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *) | |
| 24 | +val cpattern : cpattern Pcoq.Entry.t | |
| 25 | +val wit_cpattern : cpattern uniform_genarg_type | |
| 26 | + | |
| 27 | +(** OS cpattern: f _, (X in t), (t in X in t), (t as X in t) *) | |
| 28 | +val lcpattern : cpattern Pcoq.Entry.t | |
| 29 | +val wit_lcpattern : cpattern uniform_genarg_type | |
| 30 | + | |
| 31 | +(** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *) | |
| 32 | +val rpattern : rpattern Pcoq.Entry.t | |
| 33 | +val wit_rpattern : rpattern uniform_genarg_type |