diff options
| author | Maxime Dénès | 2017-06-26 21:23:29 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-26 21:23:29 +0200 |
| commit | d7189f0e97dae3f0de9641be3242552873040c44 (patch) | |
| tree | 6b926b426a0571f3b228f65a8c94c4c0a7e96c4e /theories | |
| parent | 4fbb431c81116b04e9c34cd7c6ffbf5d5f204f5e (diff) | |
| parent | d4a0e0bcc7689457340af5a3007a541b92e12301 (diff) | |
Merge PR#826: Put plugin exports in the right compatibility file
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 b30ad1af88..64ba6b1e30 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 6952fdf199..4a511d6c48 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. |