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