diff options
| author | filliatr | 2001-03-30 12:36:11 +0000 |
|---|---|---|
| committer | filliatr | 2001-03-30 12:36:11 +0000 |
| commit | 6eda1a6658dda77c5851cb1b1da4e82f11ce5fdb (patch) | |
| tree | e15da9edc563a97d68ba247029e8ca8626339ff5 /contrib/extraction/Extraction.v | |
| parent | 34fcbe510f105ed241d443fef941ba47eae041e6 (diff) | |
extraction modulaire + environnement des Fix corrigé
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1505 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/Extraction.v')
| -rw-r--r-- | contrib/extraction/Extraction.v | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v index 7a0ecd887c..a5ec0a6936 100644 --- a/contrib/extraction/Extraction.v +++ b/contrib/extraction/Extraction.v @@ -10,8 +10,11 @@ Declare ML Module "mlutil.cmo" "ocaml.cmo" "extraction.cmo" "extract_env.cmo". Grammar vernac vernac : ast := extr_constr [ "Extraction" constrarg($c) "." ] -> - [(Extraction $c)] + [ (Extraction $c) ] | extr_list [ "Extraction" "-r" ne_qualidarg_list($l) "." ] -> - [(ExtractionRec ($LIST $l))] + [ (ExtractionRec ($LIST $l)) ] | extr_list [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] -> - [(ExtractionFile $f ($LIST $l))]. + [ (ExtractionFile $f ($LIST $l)) ] +| extr_module [ "Extraction" "Module" identarg($m) "." ] -> + [ (ExtractionModule $m) ]. + |