diff options
Diffstat (limited to 'plugins/extraction/ExtrOcamlBigIntConv.v')
| -rw-r--r-- | plugins/extraction/ExtrOcamlBigIntConv.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v index c42938c8e..78ee46085 100644 --- a/plugins/extraction/ExtrOcamlBigIntConv.v +++ b/plugins/extraction/ExtrOcamlBigIntConv.v @@ -13,6 +13,8 @@ simplifies the use of [Big_int] (it can be found in the sources of Coq). *) +Require Coq.extraction.Extraction. + Require Import Arith ZArith. Parameter bigint : Type. |