nettoyage d'entrees de grammaires inutiles

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1563 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 10 insertions, 7 deletions

diff --git a/configure b/configure
index d30e9ee383..ebce54d61d 100755
--- a/configure
+++ b/configure
@@ -14,7 +14,7 @@ DATE="March 2001"
 which () {
 for i in `echo $PATH | tr ':' ' '` ; do 
   if test -z "$i"; then $i=.; fi 
-  if [ -f $i/$1 ] ; then
+  if [ -f "$i/$1" ] ; then
 	echo $i/$1
 	break
   fi
@@ -281,13 +281,13 @@ esac
 
 # do we have a native compiler: test of ocamlopt and its version
 
-if [ $best_compiler = "opt" ] ; then
+if [ "$best_compiler" = "opt" ] ; then
   CAMLOPT=`which $nativecamlc`
   case $CAMLOPT in
     "") best_compiler=byte
         echo "You have only bytecode compilation.";;
     *) CAMLOPTVERSION=`$CAMLOPT -v | sed -n -e 's|.*version* *\(.*\)$|\1|p' `
-       if [ $CAMLOPTVERSION != $CAMLVERSION ] ; then \
+       if [ "$CAMLOPTVERSION" != "$CAMLVERSION" ] ; then \
          echo "native and bytecode compilers do not have the same version!"; fi
        echo "You have native-code compilation. Good!"
   esac
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index e42223f4b6..f4edcd5440 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -102,7 +102,6 @@ GEXTEND Gram
 	  <:ast< (PrintHintDb $s) >>
       | IDENT "Print"; IDENT "Section"; s = qualidarg ->
           <:ast< (PrintSec $s) >>
-      | IDENT "Print"; IDENT "States" -> <:ast< (PrintStates) >>
       (* This should be in "syntax" section but is here for factorization *)
       | IDENT "Print"; "Grammar"; uni = identarg; ent = identarg ->
           <:ast< (PrintGrammar $uni $ent) >>
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 0ec5584faf..7ed3f645b1 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -404,7 +404,7 @@ GEXTEND Gram
     [ [ "Load"; verbosely = [ IDENT "Verbose" -> "Verbose" | -> "" ];
 	s = [ s = STRING -> s | s = IDENT -> s ] ->
           <:ast< (LoadFile ($STR $verbosely) ($STR $s)) >>
-      | "Compile";
+(*      | "Compile";
 	verbosely =
           [ IDENT "Verbose" -> "Verbose"
           | -> "" ];
@@ -417,6 +417,7 @@ GEXTEND Gram
           let fname = match fname with Some s -> s | None -> mname in
             <:ast< (CompileFile ($STR $verbosely) ($STR $only_spec)
                       ($STR $mname) ($STR $fname))>>
+*)
       | IDENT "Read"; IDENT "Module"; id = identarg ->
           <:ast< (ReadModule $id) >>
       | IDENT "Require"; import = import_tok; specif = specif_tok;
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index eae7fdf689..9c2c88eebc 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -103,14 +103,14 @@ let rec vernac interpfun input =
           let verbosely = verbosely = "Verbose" in
           raw_load_vernac_file verbosely (make_suffix fname ".v")
             
-      | Node (_,"CompileFile",[Str(_,verbosely); Str(_,only_spec);
+(*      | Node (_,"CompileFile",[Str(_,verbosely); Str(_,only_spec);
 			       Str (_,mname); Str(_,fname)]) ->
           let verbosely = verbosely = "Verbose" in
           let only_spec = only_spec = "Specification" in
           States.with_heavy_rollback (* to roll back in case of error *)
             (raw_compile_module verbosely only_spec mname)
             (make_suffix fname ".v")
-	    
+*)	    
       | Node(_,"VernacList",l) ->
 	  List.iter interp l
 
@@ -131,7 +131,9 @@ let rec vernac interpfun input =
 and raw_load_vernac_file verbosely s =
   let _ = read_vernac_file verbosely s in ()
 
+(*
 and raw_compile_module verbosely only_spec mname file =
+  assert false; (* I bet this code is never used in practice. Judicael. *)
   Library.import_module mname; (* ??? *)
   let lfname = read_vernac_file verbosely file in
   let base = Filename.chop_suffix lfname ".v" in
@@ -140,6 +142,7 @@ and raw_compile_module verbosely only_spec mname file =
     failwith ".vi not yet implemented"
   else 
     Discharge.save_module_to mname base
+*)
 
 and read_vernac_file verbosely s =
   let interpfun =