From cb1ae314411d78952062e5092804b85d981ad6e1 Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 12 Mar 2003 17:49:21 +0000
Subject: *** empty log message ***

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_proofsnew.ml4 | 126 ++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 126 insertions(+)
 create mode 100644 parsing/g_proofsnew.ml4

(limited to 'parsing/g_proofsnew.ml4')

diff --git a/parsing/g_proofsnew.ml4 b/parsing/g_proofsnew.ml4
new file mode 100644
index 000000000..db8da7101
--- /dev/null
+++ b/parsing/g_proofsnew.ml4
@@ -0,0 +1,126 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(* $Id$ *)
+
+open Pcoq
+open Pp
+open Tactic
+open Util
+open Vernac_
+open Topconstr
+open Vernacexpr
+open Prim
+open Constr
+
+let thm_token = G_vernacnew.thm_token
+
+(* Proof commands *)
+GEXTEND Gram
+  GLOBAL: command;
+
+  destruct_location :
+  [ [ IDENT "Conclusion"  -> Tacexpr.ConclLocation ()
+    | discard = [ IDENT "Discardable" -> true | -> false ]; IDENT "Hypothesis"
+	-> Tacexpr.HypLocation discard ] ]
+  ;
+  opt_hintbases:
+  [ [ -> []
+    | ":"; l = LIST1 IDENT -> l ] ]
+  ;
+  command:
+    [ [ IDENT "Goal"; c = Constr.lconstr -> VernacGoal c
+      | IDENT "Proof" -> VernacNop
+      | 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 "Qed" -> VernacEndProof (true,None)
+      | IDENT "Save" -> VernacEndProof (true,None)
+      | IDENT "Save"; tok = thm_token; id = base_ident ->
+	  VernacEndProof (true,Some (id,Some tok))
+      | IDENT "Save"; id = base_ident -> VernacEndProof (true,Some (id,None))
+      | IDENT "Defined" -> VernacEndProof (false,None)
+      |	IDENT "Defined"; id=base_ident -> VernacEndProof (false,Some (id,None))
+      | IDENT "Suspend" -> VernacSuspend
+      | IDENT "Resume" -> VernacResume None
+      | IDENT "Resume"; id = identref -> VernacResume (Some id)
+      | IDENT "Restart" -> VernacRestart
+      | IDENT "Proof"; c = Constr.lconstr -> VernacExactProof c
+      | IDENT "Undo" -> VernacUndo 1
+      | IDENT "Undo"; n = natural -> VernacUndo n
+      | IDENT "Focus" -> VernacFocus None
+      | IDENT "Focus"; n = natural -> VernacFocus (Some n)
+      | 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 "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"; IDENT "Proof" -> VernacShow ShowProof
+      | IDENT "Show"; IDENT "Intro" -> VernacShow (ShowIntros false)
+      | IDENT "Show"; IDENT "Intros" -> VernacShow (ShowIntros true)
+      | IDENT "Explain"; IDENT "Proof"; l = LIST0 integer ->
+	  VernacShow (ExplainProof l)
+      | 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
+      | IDENT "Go"; IDENT "prev" -> VernacGo GoPrev
+      | IDENT "Go"; IDENT "next" -> VernacGo GoNext
+      | IDENT "Guarded" -> VernacCheckGuard
+(* Hints for Auto and EAuto *)
+
+      | IDENT "HintDestruct"; 
+          dloc = destruct_location;
+          id  = base_ident;
+          hyptyp = Constr.constr_pattern;
+          pri = natural;
+          "["; tac = tactic; "]" -> 
+	    VernacHintDestruct (id,dloc,hyptyp,pri,tac)
+
+      | IDENT "Hint"; hintname = base_ident; dbnames = opt_hintbases; ":="; h = hint
+          -> VernacHints (dbnames, h hintname)
+	  
+      | IDENT "Hints"; (dbnames,h) = hints -> VernacHints (dbnames, h)
+	  
+
+(*This entry is not commented, only for debug*)
+      | IDENT "PrintConstr"; c = Constr.constr -> 
+	  VernacExtend ("PrintConstr",
+	    [Genarg.in_gen Genarg.rawwit_constr c])
+      ] ];
+
+  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 (n,c)
+      | IDENT "Extern"; n = natural; c = Constr.constr ; tac = tactic ->
+	  fun name -> HintsExtern (name,n,c,tac) ] ]
+  ;
+  hints:
+    [ [ IDENT "Resolve"; l = LIST1 global; dbnames = opt_hintbases ->
+         (dbnames, HintsResolve (List.map (fun qid -> (None, CRef qid)) l))
+      | IDENT "Immediate"; l = LIST1 global; dbnames = opt_hintbases ->
+        (dbnames, HintsImmediate (List.map (fun qid -> (None, CRef qid)) l))
+      | IDENT "Unfold"; l = LIST1 global; dbnames = opt_hintbases ->
+        (dbnames, HintsUnfold (List.map (fun qid -> (None,qid)) l)) ] ]
+    ;
+  constr_body:
+    [ [ ":="; c = lconstr -> c
+      | ":"; t = lconstr; ":="; c = lconstr -> CCast(loc,c,t) ] ]
+  ;
+END
-- 
cgit v1.2.3