From bb76b246d1396f788d18888abe8284befb7f44b9 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Tue, 3 Apr 2001 08:04:19 +0000
Subject: utilisation de Options.if_verbose

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1519 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/extraction/Extraction.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib')

diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v
index a5ec0a6936..1f71ef2f24 100644
--- a/contrib/extraction/Extraction.v
+++ b/contrib/extraction/Extraction.v
@@ -11,7 +11,7 @@ Declare ML Module "mlutil.cmo" "ocaml.cmo" "extraction.cmo" "extract_env.cmo".
 Grammar vernac vernac : ast :=
   extr_constr [ "Extraction" constrarg($c) "." ] -> 
               [ (Extraction $c) ]
-| extr_list   [ "Extraction" "-r" ne_qualidarg_list($l) "." ] ->
+| extr_list   [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] ->
               [ (ExtractionRec ($LIST $l)) ]
 | extr_list   [ "Extraction" stringarg($f) ne_qualidarg_list($l) "." ] ->
               [ (ExtractionFile $f ($LIST $l)) ]
-- 
cgit v1.2.3