diff options
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. |