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 /theories | |
| 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.
Diffstat (limited to 'theories')
| -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. |