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/Compat/Coq85.v | |
| 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/Compat/Coq85.v')
| -rw-r--r-- | theories/Compat/Coq85.v | 3 |
1 files changed, 0 insertions, 3 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. |