Skip to content
Snippets Groups Projects
Commit 2cd1aba1 authored by Samuel Hym's avatar Samuel Hym
Browse files

Require Extraction 

This is required in Coq 8.9
parent 34f80b6e
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 1 addition and 0 deletions
example/Extraction.v
+ 1
− 0
View file @ 2cd1aba1
...@@ -29,6 +29,7 @@ ...@@ -29,6 +29,7 @@
describe sequential computations. *) describe sequential computations. *)
Require Import Internals Example. Require Import Internals Example.
Require Extraction.
Extraction Language JSON. Extraction Language JSON.
Extraction Library Internals. Extraction Library Internals.
Extraction Library Example. Extraction Library Example.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment