diff options
| author | filliatr | 2001-04-10 13:21:45 +0000 |
|---|---|---|
| committer | filliatr | 2001-04-10 13:21:45 +0000 |
| commit | 2bb2d480b547e58deb2ec62791c8990ecac777b0 (patch) | |
| tree | 64dafd639dab62bf0c15cda96b9cab129c9c726a /contrib/extraction/Extraction.v | |
| parent | 8eaf1799ec07bf823a366920e39d79e827f94971 (diff) | |
réparation Correctness; options Extraction (changement de syntaxe)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1571 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/Extraction.v')
| -rw-r--r-- | contrib/extraction/Extraction.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v index c4c62b3cbe..e909d45111 100644 --- a/contrib/extraction/Extraction.v +++ b/contrib/extraction/Extraction.v @@ -12,10 +12,10 @@ Grammar vernac vernac : ast := | extr_list [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] -> [ (ExtractionRec ($LIST $l)) ] | extr_list - [ "Extraction" options($o) stringarg($f) ne_qualidarg_list($l) "." ] + [ "Extraction" stringarg($f) options($o) ne_qualidarg_list($l) "." ] -> [ (ExtractionFile $o $f ($LIST $l)) ] | extr_module - [ "Extraction" options($o) "Module" identarg($m) "." ] + [ "Extraction" "Module" options($o) identarg($m) "." ] -> [ (ExtractionModule $o $m) ] | extract_constant @@ -39,7 +39,7 @@ with idorstring : ast := | ids_string [ stringarg($s) ] -> [ $s ] with options : ast := -| ext_opt_noopt [ "noopt" ] -> [ (VERNACARGLIST "noopt") ] -| ext_op_expand [ "expand" "[" ne_qualidarg_list($l) "]" ] -> +| ext_opt_noopt [ "[" "noopt" "]" ] -> [ (VERNACARGLIST "noopt") ] +| ext_op_expand [ "[" "expand" ne_qualidarg_list($l) "]" ] -> [ (VERNACARGLIST "expand" ($LIST $l)) ] | ext_opt_none [ ] -> [ (VERNACARGLIST "nooption") ]. |