Add a guard for V7 mode, CVS compiles cleanly again :)

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

1 files changed, 31 insertions, 118 deletions

diff --git a/contrib/subtac/sparser.ml4 b/contrib/subtac/sparser.ml4
index c89208ae4..b2dffa28f 100644
--- a/contrib/subtac/sparser.ml4
+++ b/contrib/subtac/sparser.ml4
@@ -44,7 +44,7 @@ module Subtac =
     (* Hack to parse "(x:=t)" as an explicit argument without conflicts with the *)
     (* admissible notation "(x t)" 
        taken from g_constrnew.ml4 *)
-    let lpar_id_coloneq =
+    let test_lpar_id_coloneq =
       Gram.Entry.of_parser "test_lpar_id_coloneq"
 	(fun strm ->
 	   Pp.msgnl (Pp.str ("Testing lpar_id_coloneq:" ^ 
@@ -63,7 +63,7 @@ module Subtac =
 		    | _ -> raise Stream.Failure)
              | _ -> raise Stream.Failure)
 
-    let id_coloneq =
+    let test_id_coloneq =
       Gram.Entry.of_parser "test_id_coloneq"
 	(fun strm ->
 	   Pp.msgnl (Pp.str ("Testing id_coloneq:" ^ 
@@ -78,25 +78,13 @@ module Subtac =
                          Names.id_of_string s
 		     | _ -> raise Stream.Failure)
 	      | _ -> raise Stream.Failure))
-	     
-    (*let identifier = gec "identifier"
-    let name = gec "name"
-      let type_ident = gec "type_ident"
-      let term_ident = gec "term_ident"
-  (* binders *)
-      let binder  = gec "binder"
-      let binder_opt = gec "binder_opt"
-  (*let binders  = gec "binders"*)
-    (* programs *)
-    let term = gec "term"
-    let arg = gec "arg"
-    let name = gec "name"*)
 end 
 
 open Subtac
 open Util
 open Coqast
 
+if not !Options.v7 then
 GEXTEND Gram
   GLOBAL: subtac_spec subtac_term;
 
@@ -112,13 +100,14 @@ GEXTEND Gram
   subtac_spec_no_app: 
     [ [      
 	  "(" ; t = subtac_spec_lpar_open -> t
-	| "[" ; x = binder_opt; "]"; t = subtac_spec -> loc, TSigma (x, t)
-	| "{" ; x = binder; "|"; p = subtac_spec; "}"; "->"; t = subtac_spec ->
+	| "[" ; x = subtac_binder_opt; "]"; t = subtac_spec -> 
+	    loc, TSigma (x, t)
+	| "{" ; x = subtac_binder; "|"; p = subtac_spec; "}"; "->"; t = subtac_spec ->
 	    let ((locx, i), tx) = x in
 	      loc, TPi (((locx, Name i), (loc, TSubset (x, p))), t)
-	| "{" ; x = binder; "|"; p = subtac_spec; "}" ->
+	| "{" ; x = subtac_binder; "|"; p = subtac_spec; "}" ->
 	    loc, TSubset(x, p)
-	| t = type_ident; f = subtac_spec_tident -> f t
+	| t = subtac_type_ident; f = subtac_spec_tident -> f t
 	]
     ]
   ;
@@ -138,7 +127,7 @@ GEXTEND Gram
 
   subtac_spec_lpar_open:
     [
-      [ s = identifier; t = subtac_spec_lpar_name -> t s 
+      [ s = subtac_identifier; t = subtac_spec_lpar_name -> t s 
       | s = subtac_spec; ")" -> s ]
     ]
   ;
@@ -155,46 +144,38 @@ GEXTEND Gram
     ]
   ;
 
-  binder:
-    [ [ s = identifier; ":"; t = subtac_spec -> let (l,s) = s in
+  subtac_binder:
+    [ [ s = subtac_identifier; ":"; t = subtac_spec -> let (l,s) = s in
 	  ((loc, s), t) 
-    | "{"; x = binder; "|"; p = subtac_spec; "}" -> 
+    | "{"; x = subtac_binder; "|"; p = subtac_spec; "}" -> 
 	let ((l, s), t) = x in 
 	  ((l, s), (loc, TSubset (x, p)))
       ]
     ]
   ;
 
-  identifier:
+  subtac_identifier:
     [ [ s = IDENT -> (loc, id_of_string s) ] ]
   ;
 
-  name':
+  subtac_real_name:
     [ [ s = IDENT -> (loc, Name (id_of_string s))
-      | "_" -> loc, Anonymous
+      (* | "_" -> loc, Anonymous111 *)
       ] ]
   ;
   
-  name:
-    [ [ n = OPT name' -> match n with Some n -> n | None -> loc, Anonymous ] ]
+  subtac_name:
+    [ [ n = OPT subtac_real_name -> match n with Some n -> n | None -> loc, Anonymous ] ]
   ;
   
-  binder_opt:
-    [ [ s = name; ":"; t = subtac_spec -> (s, t) ] ]
+  subtac_binder_opt:
+    [ [ s = subtac_name; ":"; t = subtac_spec -> (s, t) ] ]
   ;
   
-  type_ident:
-    [ [ s = identifier -> loc, TIdent s ] ]
+  subtac_type_ident:
+    [ [ s = subtac_identifier -> loc, TIdent s ] ]
   ;
 
-(*   term_ident: *)
-(*     [ [ s = identifier -> SIdent s ] ] *)
-(*   ; *)
-  
-(*   lpar_colon_id: *)
-(*     [ [ i = lpar_id_coloneq -> loc, i ] ] *)
-(*   ; *)
-
   subtac_term:
     [ 
       "20" LEFTA
@@ -204,112 +185,44 @@ GEXTEND Gram
 	]
     | "10"
     	[ 
-	  i = identifier -> loc, SIdent i
-	| "fun"; bl = LIST1 binder; "=>"; p = subtac_term ->
+	  i = subtac_identifier -> loc, SIdent i
+	| "fun"; bl = LIST1 subtac_binder; "=>"; p = subtac_term ->
 	    (List.fold_left 
 	       (fun acc (((loc, s), (loc', t)) as b) -> 
 		  (join_loc loc (fst acc), SLambda (b, acc))) p bl)
-	| "let"; "("; nl = LIST0 name SEP ","; ")" ; "="; t = subtac_term;
+	| "let"; "("; nl = LIST0 subtac_name SEP ","; ")" ; "="; t = subtac_term;
 	  "in"; t' = subtac_term ->
 	    loc, (SLetTuple (nl, t, t'))
-	| "let"; i = name; "="; t = subtac_term; "in"; t' = subtac_term ->
+	| "let"; i = subtac_name; "="; t = subtac_term; "in"; t' = subtac_term ->
 	    loc, (SLetIn (i, t, t'))
 	| "if"; b = subtac_term; "then"; t = subtac_term; "else"; t' = subtac_term ->
 	    loc, SIfThenElse (b, t, t')
-	| "("; t = lpar_term -> t
+	| "("; t = subtac_lpar_term -> t
 	]
 	
     ]
   ;
 
-  lpar_term:
+  subtac_lpar_term:
     [ [
-	x = id_coloneq; t = subtac_term; ","; 
+	x = test_id_coloneq; t = subtac_term; ","; 
 	t' = subtac_term; ":"; tt = subtac_spec; ")" ->
 	  (loc, (SSumDep (((dummy_loc, x), t), (t', tt))))
-      | t = subtac_term; f = lpar_term_term -> f t
+      | t = subtac_term; f = subtac_lpar_term_term -> f t
       ]
     ]
   ;
 
-  lpar_term_term:
+  subtac_lpar_term_term:
     [ [
 	","; t' = subtac_term; ")" ->
 	  (fun t -> loc, (SSumInf (t, t')))
       | ")" -> (fun x -> x)
       ] ]
   ;
-  (*
-  subtac_term_lpar_open_ident:
-    [ [ ":="; t = subtac_term; ","; t' = subtac_term; ":"; tt = subtac_spec; ")" ->
-	  (fun x -> (loc, (SSumDep ((x, t), (t', tt)))))
-      | t = subtac_term; ")" ->
-	  (fun x -> loc, SApp ((fst x, (SIdent x)), t))
-
-      ]
-    ]
-  ;
-
-
-  sigma_binder:
-    [ [ s = OPT subtac_annot_identifier; t = subtac_term; topt = OPT subtac_annot_type ->	  
-	  (s, t, topt) ] ]
-  ;
- 
-  subtac_annot_type:
-    [ [ ":"; t = subtac_spec -> t ] ]
-  ;
-
-  subtac_annot_identifier: 
-    [ [ s = identifier; ":=" -> s ] ]
-  ;
-*)
-(*  
-  ast1:
-    [ [ x = prog2; IDENT "or"; y = prog1  -> bool_or loc x y
-      | x = prog2; IDENT "and"; y = prog1 -> bool_and loc x y
-      | x = prog2 -> x
-      ] ]
-  ;
-  ast2:
-    [ [ IDENT "not"; x = prog3 -> bool_not loc x
-      | x = prog3 -> x
-      ] ]
-  ;
-  ast3:
-    [ [ x = prog4; rel = relation; y = prog4 -> bin_op rel loc x y
-      | x = prog4 -> x
-      ] ]
-    ;
-  ast4:
-    [ [ x = prog5; "+"; y = prog4 -> bin_op "Zplus" loc x y
-      | x = prog5; "-"; y = prog4 -> bin_op "Zminus" loc x y
-      | x = prog5 -> x
-      ] ]
-    ;
-  ast5:
-    [ [ x = prog6; "*"; y = prog5 -> bin_op "Zmult" loc x y 
-      | x = prog6 -> x
-      ] ]
-    ;
-  ast6:
-    [ [ "-"; x = prog6 -> un_op "Zopp" loc x
-      | x = ast7 -> without_effect loc x
-      ] ]
-    ;
 
-  relation:
-    [ [ "<"  -> "Z_lt_ge_bool"
-      | "<=" -> "Z_le_gt_bool"
-      | ">"  -> "Z_gt_le_bool"
-      | ">=" -> "Z_ge_lt_bool"
-      | "="  -> "Z_eq_bool"
-      | "<>" -> "Z_noteq_bool" ] ] 
-  ;
-*)
   END
-;;
-
+else (* Developped with Coq 8.0 *) ()
 
 type type_loc_argtype = (type_loc, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
 type term_loc_argtype = (term_loc, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type