From e978da8c41d8a3c19a29036d9c569fbe2a4616b0 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 16 Jun 2006 14:41:51 +0000
Subject: Imported Upstream version 8.0pl3+8.1beta

---
 parsing/pcoq.ml4 | 53 +++++++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 51 insertions(+), 2 deletions(-)

(limited to 'parsing/pcoq.ml4')

diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index d743fffa..127a911f 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pcoq.ml4 7826 2006-01-09 22:00:34Z herbelin $ i*)
+(*i $Id: pcoq.ml4 8926 2006-06-08 20:23:17Z herbelin $ i*)
 
 open Pp
 open Util
@@ -286,6 +286,55 @@ let force_entry_type (u, utab) s etyp =
   with Not_found -> 
     new_entry etyp (u, utab) s
 
+(* Tactics as arguments *)
+
+let tactic_main_level = 5
+
+let (wit_tactic0,globwit_tactic0,rawwit_tactic0) = create_arg "tactic0"
+let (wit_tactic1,globwit_tactic1,rawwit_tactic1) = create_arg "tactic1"
+let (wit_tactic2,globwit_tactic2,rawwit_tactic2) = create_arg "tactic2"
+let (wit_tactic3,globwit_tactic3,rawwit_tactic3) = create_arg "tactic3"
+let (wit_tactic4,globwit_tactic4,rawwit_tactic4) = create_arg "tactic4"
+let (wit_tactic5,globwit_tactic5,rawwit_tactic5) = create_arg "tactic5"
+
+let wit_tactic = function
+  | 0 -> wit_tactic0
+  | 1 -> wit_tactic1
+  | 2 -> wit_tactic2
+  | 3 -> wit_tactic3
+  | 4 -> wit_tactic4
+  | 5 -> wit_tactic5
+  | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+
+let globwit_tactic = function
+  | 0 -> globwit_tactic0
+  | 1 -> globwit_tactic1
+  | 2 -> globwit_tactic2
+  | 3 -> globwit_tactic3
+  | 4 -> globwit_tactic4
+  | 5 -> globwit_tactic5
+  | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+
+let rawwit_tactic = function
+  | 0 -> rawwit_tactic0
+  | 1 -> rawwit_tactic1
+  | 2 -> rawwit_tactic2
+  | 3 -> rawwit_tactic3
+  | 4 -> rawwit_tactic4
+  | 5 -> rawwit_tactic5
+  | n -> anomaly ("Unavailable tactic level: "^string_of_int n)
+
+let tactic_genarg_level s =
+  if String.length s = 7 && String.sub s 0 6 = "tactic" then
+    let c = s.[6] in if '5' >= c && c >= '0' then Some (Char.code c - 48)
+    else None
+  else None
+
+let is_tactic_genarg = function
+| ExtraArgType s -> tactic_genarg_level s <> None
+| _ -> false
+
+
 (* [make_gen_entry] builds entries extensible by giving its name (a string) *)
 (* For entries extensible only via the ML name, Gram.Entry.create is enough *)
 
@@ -382,7 +431,6 @@ module Tactic =
     let tactic_arg = Gram.Entry.create "tactic:tactic_arg"
     let tactic_expr = Gram.Entry.create "tactic:tactic_expr"
 
-    let tactic_main_level = 5
     let tactic = make_gen_entry utactic (rawwit_tactic tactic_main_level) "tactic"
 
     (* Main entry for quotations *)
@@ -391,6 +439,7 @@ module Tactic =
   end
 
 
+
 module Vernac_ =
   struct
     let gec_vernac s = Gram.Entry.create ("vernac:" ^ s)
-- 
cgit v1.2.3