Un seul binaire commun v7 et v8 avec détection précoce de l'option -v8 et choix

du parseur en fonction de cette option


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

14 files changed, 60 insertions, 10 deletions

diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index d32384c86..d8766f273 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -23,10 +23,13 @@ let vernac_kw =
     "Definition"; "Inductive"; "CoInductive"; 
     "Theorem"; "Variable"; "Axiom"; "Parameter"; "Hypothesis";
     "."; ">->" ]
-let _ = List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
+let _ = 
+  if !Options.v7 then
+    List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
 
 let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
 
+if !Options.v7 then
 GEXTEND Gram
   GLOBAL: class_rawexpr;
 
@@ -37,6 +40,7 @@ GEXTEND Gram
   ;
 END;
 
+if !Options.v7 then
 GEXTEND Gram
   GLOBAL: command;
 
@@ -219,6 +223,7 @@ let map_modl = function
   | SetLevel n -> SetLevel(adapt_level n)
   | m -> m
 	  
+if !Options.v7 then
 GEXTEND Gram
   GLOBAL: syntax;
 
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 4d4000b23..f1f6e47a4 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -19,6 +19,7 @@ open Prim
 let pair loc =
   Qualid (loc, Libnames.qualid_of_string "Coq.Init.Datatypes.pair")
 
+if !Options.v7 then
 GEXTEND Gram
   GLOBAL: operconstr pattern;
 
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 5904906b0..16e1a6388 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -25,7 +25,9 @@ let constr_kw =
     "<->"; "\\/"; "/\\"; "`"; "``"; "&"; "*"; "+"; "@"; "^"; "#"; "-";
     "~"; "'"; "<<"; ">>"; "<>"
   ]
-let _ = List.iter (fun s -> Lexer.add_token ("",s)) constr_kw
+let _ =
+  if !Options.v7 then
+  List.iter (fun s -> Lexer.add_token ("",s)) constr_kw
 (* "let" is not a keyword because #Core#let.cci would not parse.
    Is it still accurate ? *)
 
@@ -92,6 +94,7 @@ let test_ident_colon =
         | _ -> raise Stream.Failure)
 
 
+if !Options.v7 then
 GEXTEND Gram
   GLOBAL: operconstr lconstr constr sort global constr_pattern Constr.ident annot
           (*ne_name_comma_list*);
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index c34f82efa..6e279218e 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -23,8 +23,14 @@ let constr_kw =
   [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; 
     "end"; "as"; "let"; "if"; "then"; "else"; "return";
     "Prop"; "Set"; "Type"; ".(" ]
-let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw
+
+let _ = 
+  if not !Options.v7 then
+    List.iter (fun s -> Lexer.add_token("",s)) constr_kw
+
+(*
 let _ = Options.v7 := false
+*)
 
 (* For Correctness syntax; doesn't work if in psyntax (freeze pb?)  *)
 let _ = Lexer.add_token ("","!")
@@ -126,6 +132,7 @@ let rec mkCLambdaN loc bll c =
   | [] -> c
   | LocalRawAssum ([],_) :: bll -> mkCLambdaN loc bll c
 
+if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: binder_constr lconstr constr operconstr sort global
   constr_pattern Constr.ident binder_let tuple_constr;
@@ -324,4 +331,4 @@ GEXTEND Gram
   type_cstr:
     [ [ c=OPT [":"; c=lconstr -> c] -> (loc,c) ] ]
   ;
-END;;
+  END;;
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index b3fd4fa19..b342d9716 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -66,6 +66,7 @@ let arg_of_expr = function
     
 (* Tactics grammar rules *)
 
+if !Options.v7 then
 GEXTEND Gram
   GLOBAL: tactic Vernac_.command tactic_arg;
 
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4
index a32926bb1..ed6664035 100644
--- a/parsing/g_ltacnew.ml4
+++ b/parsing/g_ltacnew.ml4
@@ -68,6 +68,7 @@ open Prelude
 
 let tactic_expr = Gram.Entry.create "tactic:tactic_expr"
 
+if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: tactic Vernac_.command tactic_expr tactic_arg;
 
diff --git a/parsing/g_module.ml4 b/parsing/g_module.ml4
index a3714c43b..7e2532c20 100644
--- a/parsing/g_module.ml4
+++ b/parsing/g_module.ml4
@@ -18,6 +18,7 @@ open Topconstr
 
 (* Grammar rules for module expressions and types *)
 
+if !Options.v7 then
 GEXTEND Gram
   GLOBAL: module_expr module_type;
  
diff --git a/parsing/g_primnew.ml4 b/parsing/g_primnew.ml4
index 4ca29e232..d41055fb6 100644
--- a/parsing/g_primnew.ml4
+++ b/parsing/g_primnew.ml4
@@ -14,8 +14,11 @@ open Names
 open Libnames
 open Topconstr
 
-let _ = Pcoq.reset_all_grammars()
 let _ =
+  if not !Options.v7 then
+    Pcoq.reset_all_grammars()
+let _ =
+  if not !Options.v7 then
   let f = Gram.Unsafe.clear_entry in
   f Prim.bigint;
   f Prim.qualid;
@@ -23,7 +26,9 @@ let _ =
   f Prim.reference
 
 let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "<>"; "<<"; ">>"; "'"]
-let _ = List.iter (fun s -> Lexer.add_token("",s)) prim_kw
+let _ = 
+  if not !Options.v7 then
+    List.iter (fun s -> Lexer.add_token("",s)) prim_kw
 
 ifdef Quotify then
 open Qast
@@ -77,6 +82,7 @@ open Prelude
 ifdef Quotify then
 open Q
 
+if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: ast bigint qualid reference;
   metaident:
@@ -134,6 +140,7 @@ GEXTEND Gram
   ;
 END
 
+(*
 let constr_to_ast a =
   Termast.ast_of_rawconstr
     (Constrintern.interp_rawconstr Evd.empty (Global.env()) a)
@@ -141,3 +148,4 @@ let constr_to_ast a =
 let constr_parser_with_glob = Pcoq.map_entry constr_to_ast Constr.constr
 
 let _ = define_ast_quotation true "constr" constr_parser_with_glob
+*)
diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 0c9e0ce26..f3ef4dc76 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -21,6 +21,7 @@ open Constr
 let thm_token = Gram.Entry.create "vernac:thm_token"
 
 (* Proof commands *)
+if !Options.v7 then
 GEXTEND Gram
   GLOBAL: command;
 
diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4
index e0e374426..b8f1f2554 100644
--- a/parsing/g_proofsnew.ml4
+++ b/parsing/g_proofsnew.ml4
@@ -21,6 +21,7 @@ open Constr
 let thm_token = G_vernacnew.thm_token
 
 (* Proof commands *)
+if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: command;
 
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index c52a5888d..18422b460 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -25,7 +25,9 @@ open Tactic
 
 let tactic_kw =
   [ "using"; "Orelse"; "Proof"; "Qed"; "And"; "()"; "|-" ]
-let _ = List.iter (fun s -> Lexer.add_token ("",s)) tactic_kw
+let _ =
+  if !Options.v7 then
+    List.iter (fun s -> Lexer.add_token ("",s)) tactic_kw
 
 (* Functions overloaded by quotifier *)
 
@@ -58,6 +60,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 
 (* Auxiliary grammar rules *)
 
+if !Options.v7 then
 GEXTEND Gram
   GLOBAL: simple_tactic constrarg constr_with_bindings quantified_hypothesis
     red_expr int_or_var castedopenconstr;
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index e4810cda0..414311b0f 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -18,7 +18,9 @@ open Genarg
 
 let tactic_kw =
   [ "->"; "<-" ]
-let _ = List.iter (fun s -> Lexer.add_token("",s)) tactic_kw
+let _ = 
+  if not !Options.v7 then
+    List.iter (fun s -> Lexer.add_token("",s)) tactic_kw
 
 (* Hack to parse "with n := c ..." as a binder without conflicts with the *)
 (* admissible notation "with c1 c2..." *)
@@ -71,6 +73,7 @@ let join_to_constr loc c2 = (fst loc), snd (Topconstr.constr_loc c2)
 
 (* Auxiliary grammar rules *)
 
+if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: simple_tactic constrarg constr_with_bindings quantified_hypothesis
     red_expr int_or_var castedopenconstr;
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 19af91a80..bda234764 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -33,6 +33,7 @@ let thm_token = G_proofs.thm_token
 (* Rem: do not join the different GEXTEND into one, it breaks native *)
 (* compilation on PowerPC and Sun architectures *)
 
+if !Options.v7 then
 GEXTEND Gram
   GLOBAL: vernac gallina_ext;
   vernac:
@@ -95,6 +96,7 @@ let test_plurial_form = function
   | _ -> ()
 
 (* Gallina declarations *)
+if !Options.v7 then
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token;
 
@@ -439,6 +441,7 @@ GEXTEND Gram
 END
 
 (* Modules management *)   
+if !Options.v7 then
 GEXTEND Gram
   GLOBAL: command;
 
@@ -489,6 +492,7 @@ GEXTEND Gram
   ;
 END
 
+if !Options.v7 then
 GEXTEND Gram
   GLOBAL: command;
 
diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4
index fddda8b68..86658e2bb 100644
--- a/parsing/g_vernacnew.ml4
+++ b/parsing/g_vernacnew.ml4
@@ -29,7 +29,9 @@ open Module
 
 
 let vernac_kw = [ ";"; ","; ">->"; ":<"; "<:" ]
-let _ = List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
+let _ = 
+  if not !Options.v7 then
+    List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
 
 (* Rem: do not join the different GEXTEND into one, it breaks native *)
 (* compilation on PowerPC and Sun architectures *)
@@ -39,6 +41,7 @@ let class_rawexpr = Gram.Entry.create "vernac:class_rawexpr"
 let thm_token = Gram.Entry.create "vernac:thm_token"
 let def_body = Gram.Entry.create "vernac:def_body"
 
+if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: vernac gallina_ext;
   vernac:
@@ -91,6 +94,7 @@ let flatten_assum l =
     (List.map (fun (oc,(idl,t)) -> List.map (fun id -> (oc,(id,t))) idl) l)
 
 (* Gallina declarations *)
+if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: gallina gallina_ext thm_token def_body;
 
@@ -296,6 +300,7 @@ END
 
 
 (* Modules and Sections *)
+if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: gallina_ext module_expr module_type;
 
@@ -383,6 +388,7 @@ GEXTEND Gram
 END
 
 (* Extensions: implicits, coercions, etc. *)   
+if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: gallina_ext;
 
@@ -448,6 +454,7 @@ GEXTEND Gram
   ;
 END
 
+if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: command check_command class_rawexpr;
 
@@ -630,6 +637,7 @@ GEXTEND Gram
   ;
 END;
 
+if not !Options.v7 then
 GEXTEND Gram
   command:
     [ [ 
@@ -655,6 +663,7 @@ GEXTEND Gram
 
 (* Grammar extensions *)
 	  
+if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: syntax;
 
@@ -873,4 +882,6 @@ GEXTEND Gram
 END
 
 (* Reinstall tactic and vernac extensions *)
-let _ = Egrammar.reset_extend_grammars_v8()
+let _ = 
+  if not !Options.v7 then
+    Egrammar.reset_extend_grammars_v8()