Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 41 insertions, 54 deletions

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 5262b785..886b33e2 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_proofs.ml4,v 1.33.2.1 2004/07/16 19:30:39 herbelin Exp $ *)
+(* $Id: g_proofs.ml4 7936 2006-01-28 18:36:54Z herbelin $ *)
 
 open Pcoq
 open Pp
@@ -18,10 +18,9 @@ open Vernacexpr
 open Prim
 open Constr
 
-let thm_token = Gram.Entry.create "vernac:thm_token"
+let thm_token = G_vernac.thm_token
 
 (* Proof commands *)
-if !Options.v7 then
 GEXTEND Gram
   GLOBAL: command;
 
@@ -35,27 +34,29 @@ GEXTEND Gram
     | ":"; l = LIST1 IDENT -> l ] ]
   ;
   command:
-    [ [ IDENT "Goal"; c = Constr.constr -> VernacGoal c
-      | "Proof" -> VernacProof (Tacexpr.TacId "")
-      | "Proof"; "with"; ta = tactic -> VernacProof ta
+    [ [ IDENT "Goal"; c = lconstr -> VernacGoal c
+      | IDENT "Proof" -> VernacProof (Tacexpr.TacId [])
+      | IDENT "Proof"; "with"; ta = tactic -> VernacProof ta
       | IDENT "Abort" -> VernacAbort None
       | IDENT "Abort"; IDENT "All" -> VernacAbortAll
       | IDENT "Abort"; id = identref -> VernacAbort (Some id)
+      | IDENT "Existential"; n = natural; c = constr_body ->
+	  VernacSolveExistential (n,c)
       | IDENT "Admitted" -> VernacEndProof Admitted
-      | "Qed" -> VernacEndProof (Proved (true,None))
+      | IDENT "Qed" -> VernacEndProof (Proved (true,None))
       | IDENT "Save" -> VernacEndProof (Proved (true,None))
-      | IDENT "Defined" -> VernacEndProof (Proved (false,None))
-      |	IDENT "Defined"; id=identref -> 
-	  VernacEndProof (Proved (false,Some (id,None)))
       | IDENT "Save"; tok = thm_token; id = identref ->
 	  VernacEndProof (Proved (true,Some (id,Some tok)))
       | IDENT "Save"; id = identref ->
 	  VernacEndProof (Proved (true,Some (id,None)))
+      | IDENT "Defined" -> VernacEndProof (Proved (false,None))
+      |	IDENT "Defined"; id=identref -> 
+	  VernacEndProof (Proved (false,Some (id,None)))
       | IDENT "Suspend" -> VernacSuspend
       | IDENT "Resume" -> VernacResume None
       | IDENT "Resume"; id = identref -> VernacResume (Some id)
       | IDENT "Restart" -> VernacRestart
-      | "Proof"; c = Constr.constr -> VernacExactProof c
+      | IDENT "Proof"; c = lconstr -> VernacExactProof c
       | IDENT "Undo" -> VernacUndo 1
       | IDENT "Undo"; n = natural -> VernacUndo n
       | IDENT "Focus" -> VernacFocus None
@@ -63,20 +64,20 @@ GEXTEND Gram
       | IDENT "Unfocus" -> VernacUnfocus
       | IDENT "Show" -> VernacShow (ShowGoal None)
       | IDENT "Show"; n = natural -> VernacShow (ShowGoal (Some n))
-      | IDENT "Show"; IDENT "Implicits"; n = natural ->
-	  VernacShow (ShowGoalImplicitly (Some n))
-      | IDENT "Show"; IDENT "Implicits" -> VernacShow (ShowGoalImplicitly None)
+      | IDENT "Show"; IDENT "Implicit"; IDENT "Arguments"; n = OPT natural ->
+	  VernacShow (ShowGoalImplicitly n)
       | IDENT "Show"; IDENT "Node" -> VernacShow ShowNode
       | IDENT "Show"; IDENT "Script" -> VernacShow ShowScript
       | IDENT "Show"; IDENT "Existentials" -> VernacShow ShowExistentials
       | IDENT "Show"; IDENT "Tree" -> VernacShow ShowTree
       | IDENT "Show"; IDENT "Conjectures" -> VernacShow ShowProofNames
-      | IDENT "Show"; "Proof" -> VernacShow ShowProof
+      | IDENT "Show"; IDENT "Proof" -> VernacShow ShowProof
       | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false)
       | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true)
-      | IDENT "Explain"; "Proof"; l = LIST0 integer ->
+      | IDENT "Show"; IDENT "Match"; id = identref -> VernacShow (ShowMatch id)
+      | IDENT "Explain"; IDENT "Proof"; l = LIST0 integer ->
 	  VernacShow (ExplainProof l)
-      | IDENT "Explain"; "Proof"; IDENT "Tree"; l = LIST0 integer -> 
+      | IDENT "Explain"; IDENT "Proof"; IDENT "Tree"; l = LIST0 integer -> 
 	  VernacShow (ExplainTree l)
       | IDENT "Go"; n = natural -> VernacGo (GoTo n)
       | IDENT "Go"; IDENT "top" -> VernacGo GoTop
@@ -84,26 +85,13 @@ GEXTEND Gram
       | IDENT "Go"; IDENT "next" -> VernacGo GoNext
       | IDENT "Guarded" -> VernacCheckGuard
 (* Hints for Auto and EAuto *)
-
-      | IDENT "HintDestruct"; 
-	  local = locality;
-          dloc = destruct_location;
-          id  = base_ident;
-          hyptyp = Constr.constr_pattern;
-          pri = natural;
-          "["; tac = tactic; "]" -> 
-	    VernacHints(local,[],HintsDestruct (id,pri,dloc,hyptyp,tac))
-
-      | IDENT "Hint"; local = locality; hintname = base_ident; 
-	  dbnames = opt_hintbases; ":="; h = hint
-          -> VernacHints (local,dbnames, h hintname)
-	  
-      | IDENT "Hints"; local = locality; 
-	  (dbnames,h) = hints -> VernacHints (local,dbnames, h)
+      | IDENT "Hint"; local = locality; h = hint;
+        dbnames = opt_hintbases ->
+	  VernacHints (local,dbnames, h)
 	  
 
 (*This entry is not commented, only for debug*)
-      | IDENT "PrintConstr"; c = Constr.constr -> 
+      | IDENT "PrintConstr"; c = constr -> 
 	  VernacExtend ("PrintConstr",
 	    [Genarg.in_gen Genarg.rawwit_constr c])
       ] ];
@@ -112,24 +100,23 @@ GEXTEND Gram
     [ [ IDENT "Local" -> true | -> false ] ]
   ;
   hint:
-    [ [ IDENT "Resolve"; c = Constr.constr -> fun name -> HintsResolve [Some name, c]
-      | IDENT "Immediate"; c = Constr.constr -> fun name -> HintsImmediate [Some name, c]
-      | IDENT "Unfold"; qid = global -> fun name -> HintsUnfold [Some name,qid]
-      | IDENT "Constructors"; c = global -> fun n ->
-          HintsConstructors (Some n,[c])
-      | IDENT "Extern"; n = natural; c = Constr.constr ; tac = tactic ->
-	  fun name -> HintsExtern (Some name,n,c,tac) ] ]
-  ;
-  hints:
-    [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases ->
-         (dbnames, 
-	  HintsResolve
-	    (List.map (fun qid -> (None, CAppExpl(loc,(None,qid),[]))) l))
-      | IDENT "Immediate"; l = LIST1 global; dbnames = opt_hintbases ->
-        (dbnames, 
-	 HintsImmediate
-	   (List.map (fun qid-> (None, CAppExpl (loc,(None,qid),[]))) l))
-      | IDENT "Unfold"; l = LIST1 global; dbnames = opt_hintbases ->
-        (dbnames, HintsUnfold (List.map (fun qid -> (None,qid)) l)) ] ]
+    [ [ IDENT "Resolve"; lc = LIST1 constr -> HintsResolve lc
+      | IDENT "Immediate"; lc = LIST1 constr -> HintsImmediate lc
+      | IDENT "Unfold"; lqid = LIST1 global -> HintsUnfold lqid
+      | IDENT "Constructors"; lc = LIST1 global -> HintsConstructors lc
+      | IDENT "Extern"; n = natural; c = constr_pattern ; "=>";
+          tac = tactic ->
+	  HintsExtern (n,c,tac)
+      | IDENT "Destruct"; 
+          id = ident; ":=";
+          pri = natural;
+          dloc = destruct_location;
+          hyptyp = constr_pattern;
+          "=>"; tac = tactic ->
+            HintsDestruct(id,pri,dloc,hyptyp,tac) ] ]
     ;
-  END
+  constr_body:
+    [ [ ":="; c = lconstr -> c
+      | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,Term.DEFAULTcast,t) ] ]
+  ;
+END