diff options
Diffstat (limited to 'parsing/pcoq.ml4')
| -rw-r--r-- | parsing/pcoq.ml4 | 53 |
1 files changed, 51 insertions, 2 deletions
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) |