diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-06-15 18:34:26 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-06-22 21:06:24 -0400 |
| commit | ee8385ef39292fd03bdbae3a7a73726d9fb65e99 (patch) | |
| tree | eaba2ab99aeb3529d7a14310a1fe9906a3b955e1 | |
| parent | 8d92701f1a017354504c84d60c9e76da50feaf49 (diff) | |
Put plugin exports in the right compatibility file
This closes [bug #5607](https://coq.inria.fr/bugs/show_bug.cgi?id=5607).
PR #220 put the exports in the wrong compat files, presumably because it
was originally targeted to version 8.6, and this wasn't updated when it
was retargeted to version 8.7.
| -rw-r--r-- | theories/Compat/Coq85.v | 3 | ||||
| -rw-r--r-- | theories/Compat/Coq86.v | 4 |
2 files changed, 3 insertions, 4 deletions
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index b30ad1af8..64ba6b1e3 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -34,6 +34,3 @@ Global Unset Typeclasses Filtered Unification. (** Allow silently letting unification constraints float after a "." *) Global Unset Solve Unification Constraints. - -Require Export Coq.extraction.Extraction. -Require Export Coq.funind.FunInd. diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq86.v index 6952fdf19..4a511d6c4 100644 --- a/theories/Compat/Coq86.v +++ b/theories/Compat/Coq86.v @@ -6,4 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Compatibility file for making Coq act similar to Coq v8.6 *)
\ No newline at end of file +(** Compatibility file for making Coq act similar to Coq v8.6 *) +Require Export Coq.extraction.Extraction. +Require Export Coq.funind.FunInd. |