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