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_ltac.ml4 | 42 ++++++++++++++++++++++++++----------------
 1 file changed, 26 insertions(+), 16 deletions(-)

(limited to 'parsing/g_ltac.ml4')

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index c01c23b6..27ff8140 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: g_ltac.ml4 9037 2006-07-11 12:43:50Z herbelin $ *)
+(* $Id: g_ltac.ml4 9333 2006-11-02 13:59:14Z barras $ *)
 
 open Pp
 open Util
@@ -43,38 +43,34 @@ let tacarg_of_expr = function
 (* Tactics grammar rules *)
 
 GEXTEND Gram
-  GLOBAL: tactic Vernac_.command tactic_expr tactic_arg constr_may_eval;
+  GLOBAL: tactic Vernac_.command tactic_expr binder_tactic tactic_arg
+          constr_may_eval;
 
   tactic_expr:
-    [ "5" LEFTA
-      [ ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1)
+    [ "5" RIGHTA
+      [ te = binder_tactic -> te ]
+    | "4" LEFTA
+      [ ta0 = tactic_expr; ";"; ta1 = binder_tactic -> TacThen (ta0, ta1)
+      | ta0 = tactic_expr; ";"; ta1 = tactic_expr -> TacThen (ta0, ta1)
       | ta = tactic_expr; ";"; 
 	"["; lta = LIST0 OPT tactic_expr SEP "|"; "]" ->
 	  let lta = List.map (function None -> TacId [] | Some t -> t) lta in 
 	  TacThens (ta, lta) ]
-    | "4"
-      [ ]
     | "3" RIGHTA
       [ IDENT "try"; ta = tactic_expr -> TacTry ta
       | IDENT "do"; n = int_or_var; ta = tactic_expr -> TacDo (n,ta)
       | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
       | IDENT "progress"; ta = tactic_expr -> TacProgress ta
-      | IDENT "info"; tc = tactic_expr -> TacInfo tc
 (*To do: put Abstract in Refiner*)
       | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
       | IDENT "abstract"; tc = NEXT; "using";  s = ident ->
           TacAbstract (tc,Some s) ]
 (*End of To do*)
     | "2" RIGHTA
-      [ ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
+      [ ta0 = tactic_expr; "||"; ta1 = binder_tactic -> TacOrelse (ta0,ta1)
+      | ta0 = tactic_expr; "||"; ta1 = tactic_expr -> TacOrelse (ta0,ta1) ]
     | "1" RIGHTA
-      [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr ->
-          TacFun (it,body)
-      | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in";
-          body = tactic_expr -> TacLetRecIn (rcl,body)
-      | "let"; llc = LIST1 let_clause SEP "with"; "in";
-          u = tactic_expr -> TacLetIn (make_letin_clause loc llc,u)
-      | b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
+      [ b = match_key; IDENT "goal"; "with"; mrl = match_context_list; "end" ->
           TacMatchContext (b,false,mrl)
       | b = match_key; IDENT "reverse"; IDENT "goal"; "with";
         mrl = match_context_list; "end" ->
@@ -104,6 +100,17 @@ GEXTEND Gram
       [ "("; a = tactic_expr; ")" -> a
       | a = tactic_atom -> TacArg a ] ]
   ;
+  (* binder_tactic: level 5 of tactic_expr *)
+  binder_tactic:
+    [ RIGHTA
+      [ "fun"; it = LIST1 input_fun ; "=>"; body = tactic_expr LEVEL "5" ->
+          TacFun (it,body)
+      | "let"; IDENT "rec"; rcl = LIST1 rec_clause SEP "with"; "in";
+          body = tactic_expr LEVEL "5" -> TacLetRecIn (rcl,body)
+      | "let"; llc = LIST1 let_clause SEP "with"; "in";
+          u = tactic_expr LEVEL "5" -> TacLetIn (make_letin_clause loc llc,u)
+      | IDENT "info"; tc = tactic_expr LEVEL "5" -> TacInfo tc ] ]
+  ;
   (* Tactic arguments *)
   tactic_arg:
     [ [ IDENT "ltac"; ":"; a = tactic_expr LEVEL "0" -> tacarg_of_expr a
@@ -115,7 +122,10 @@ GEXTEND Gram
   ;
   may_eval_arg:
     [ [ c = constr_eval -> ConstrMayEval c
-      | IDENT "fresh"; s = OPT STRING -> TacFreshId s ] ]
+      | IDENT "fresh"; l = LIST0 fresh_id -> TacFreshId l ] ]
+  ;
+  fresh_id:
+    [ [ s = STRING -> ArgArg s | id = ident -> ArgVar (loc,id) ] ]
   ;
   constr_eval:
     [ [ IDENT "eval"; rtc = red_expr; "in"; c = Constr.constr ->
-- 
cgit v1.2.3