diff options
Diffstat (limited to 'doc/Extraction.tex')
| -rwxr-xr-x | doc/Extraction.tex | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/doc/Extraction.tex b/doc/Extraction.tex index 0ad4410b1..629b84530 100755 --- a/doc/Extraction.tex +++ b/doc/Extraction.tex @@ -369,7 +369,7 @@ We can now extract this program to \ocaml: Reset Initial. \end{coq_eval} \begin{coq_example} -Require Euclid. +Require Import Euclid. Extraction Inline Wf_nat.gt_wf_rec Wf_nat.lt_wf_rec. Recursive Extraction eucl_dev. \end{coq_example} @@ -421,13 +421,13 @@ treesort}, whose type is shown below: \begin{coq_eval} Reset Initial. -Require Relation_Definitions. -Require List. -Require Sorting. -Require Permutation. +Require Import Relation_Definitions. +Require Import List. +Require Import Sorting. +Require Import Permutation. \end{coq_eval} \begin{coq_example} -Require Heap. +Require Import Heap. Check treesort. \end{coq_example} |