From 208a0f7bfa5249f9795e6e225f309cbe715c0fad Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Tue, 21 Nov 2006 21:38:49 +0000
Subject: Imported Upstream version 8.1~gamma

---
 parsing/g_vernac.ml4 | 62 ++++++++++++++++++++++++++++++++++++++--------------
 1 file changed, 46 insertions(+), 16 deletions(-)

(limited to 'parsing/g_vernac.ml4')

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index a72ced97..9bbdc1d4 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_vernac.ml4 9017 2006-07-05 17:27:34Z herbelin $ *)
+(* $Id: g_vernac.ml4 9306 2006-10-28 18:28:19Z herbelin $ *)
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
 open Pp
@@ -15,6 +15,7 @@ open Names
 open Topconstr
 open Vernacexpr
 open Pcoq
+open Decl_mode
 open Tactic
 open Decl_kinds
 open Genarg
@@ -34,13 +35,28 @@ let _ = List.iter (fun s -> Lexer.add_token ("",s)) vernac_kw
 (* compilation on PowerPC and Sun architectures *)
 
 let check_command = Gram.Entry.create "vernac:check_command"
+
+let tactic_mode = Gram.Entry.create "vernac:tactic_command"
+let proof_mode = Gram.Entry.create "vernac:proof_command"
+let noedit_mode = Gram.Entry.create "vernac:noedit_command"
+
 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"
 
+let get_command_entry () =
+  match Decl_mode.get_current_mode () with
+      Mode_proof -> proof_mode
+    | Mode_tactic -> tactic_mode
+    | Mode_none -> noedit_mode
+
+let default_command_entry =
+  Gram.Entry.of_parser "command_entry" 
+    (fun strm -> Gram.Entry.parse_token (get_command_entry ()) strm)
+
 let no_hook _ _ = ()
 GEXTEND Gram
-  GLOBAL: vernac gallina_ext;
+  GLOBAL: vernac gallina_ext tactic_mode proof_mode noedit_mode;
   vernac:
     (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
     (* "." is still in the stream and discard_to_dot works correctly         *)
@@ -54,9 +70,15 @@ GEXTEND Gram
   vernac: FIRST
     [ [ IDENT "Time"; v = vernac  -> VernacTime v ] ]
   ;
-  vernac: LAST
-    [ [ gln = OPT[n=natural; ":" -> n];
-        tac = subgoal_command -> tac gln ] ]
+  vernac: LAST  
+    [ [ prfcom = default_command_entry -> prfcom ] ]
+  ;
+  noedit_mode:
+    [ [ c = subgoal_command -> c None] ]
+  ;
+  tactic_mode:
+  [ [ gln = OPT[n=natural; ":" -> n];
+      tac = subgoal_command -> tac gln ] ]
   ;
   subgoal_command:
     [ [ c = check_command; "." -> c
@@ -66,6 +88,12 @@ GEXTEND Gram
             let g = match g with Some gl -> gl | _ -> 1 in
             VernacSolve(g,tac,use_dft_tac)) ] ]
   ;
+  proof_mode:
+    [ [ instr = proof_instr; "." -> VernacProofInstr instr ] ] 
+  ;
+  proof_mode: LAST
+    [ [ c=subgoal_command -> c (Some 1) ] ]
+  ; 
   located_vernac:
     [ [ v = vernac -> loc, v ] ]
   ;
@@ -191,9 +219,9 @@ GEXTEND Gram
     ;
   (* Inductives and records *)
   inductive_definition:
-    [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr; 
+    [ [ id = identref; indpar = LIST0 binder_let; ":"; c = lconstr;
         ":="; lc = constructor_list; ntn = decl_notation ->
-	  (id,ntn,indpar,c,lc) ] ]
+	  ((id,indpar,c,lc),ntn) ] ]
   ;
   constructor_list:
     [ [ "|"; l = LIST1 constructor SEP "|" -> l
@@ -212,7 +240,7 @@ GEXTEND Gram
   (* (co)-fixpoints *)
   rec_definition:
     [ [ id = ident; bl = LIST1 binder_let;
-        annot = rec_annotation; type_ = type_cstr; 
+        annot = rec_annotation; ty = type_cstr; 
 	":="; def = lconstr; ntn = decl_notation ->
           let names = List.map snd (names_of_local_assums bl) in
           let ni =
@@ -227,12 +255,12 @@ GEXTEND Gram
 		     otherwise, we search the recursive index later *)
 		  if List.length names = 1 then Some 0 else None	  
 	  in 
-	  ((id, (ni, snd annot), bl, type_, def),ntn) ] ]
+	  ((id,(ni,snd annot),bl,ty,def),ntn) ] ]
   ;
   corec_definition:
-    [ [ id = ident; bl = LIST0 binder_let; c = type_cstr; ":=";
-        def = lconstr ->
-          (id,bl,c ,def) ] ]
+    [ [ id = ident; bl = LIST0 binder_let; ty = type_cstr; ":=";
+        def = lconstr; ntn = decl_notation ->
+          ((id,bl,ty,def),ntn) ] ]
   ;
   rec_annotation:
     [ [ "{"; IDENT "struct"; id=IDENT; "}" -> (Some (id_of_string id), CStructRec)
@@ -460,9 +488,8 @@ GEXTEND Gram
       | IDENT "Declare"; IDENT "ML"; IDENT "Module"; l = LIST1 ne_string ->
 	  VernacDeclareMLModule l
 
-      (* Dump of the universe graph - to file or to stdout *) 
       | IDENT "Dump"; IDENT "Universes"; fopt = OPT ne_string ->
-	  VernacPrint (PrintUniverses fopt)
+	  error "This command is deprecated, use Print Universes"
 
       | IDENT "Locate"; l = locatable -> VernacLocate l
 
@@ -556,7 +583,9 @@ GEXTEND Gram
       | IDENT "Remove"; table = IDENT; field = IDENT; v= LIST1 option_ref_value
         -> VernacRemoveOption (SecondaryTable (table,field), v)
       | IDENT "Remove"; table = IDENT; v = LIST1 option_ref_value ->
-	  VernacRemoveOption (PrimaryTable table, v) ] ]
+	  VernacRemoveOption (PrimaryTable table, v) 
+      | IDENT "proof" -> VernacDeclProof
+      | "return" -> VernacReturn ]]
   ;
   check_command: (* TODO: rapprocher Eval et Check *)
     [ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
@@ -596,7 +625,8 @@ GEXTEND Gram
       | IDENT "Scopes" -> PrintScopes
       | IDENT "Scope"; s = IDENT -> PrintScope s
       | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
-      | IDENT "Implicit"; qid = global -> PrintImplicit qid ] ]
+      | IDENT "Implicit"; qid = global -> PrintImplicit qid
+      | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt ] ]
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
-- 
cgit v1.2.3