summaryrefslogtreecommitdiff
path: root/parsing/pcoq.mli
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2006-06-16 14:41:51 +0000
commite978da8c41d8a3c19a29036d9c569fbe2a4616b0 (patch)
tree0de2a907ee93c795978f3c843155bee91c11ed60 /parsing/pcoq.mli
parent3ef7797ef6fc605dfafb32523261fe1b023aeecb (diff)
Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta
Diffstat (limited to 'parsing/pcoq.mli')
-rw-r--r--parsing/pcoq.mli41
1 files changed, 38 insertions, 3 deletions
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index fe6fd083..3998d71b 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: pcoq.mli 7826 2006-01-09 22:00:34Z herbelin $ i*)
+(*i $Id: pcoq.mli 8926 2006-06-08 20:23:17Z herbelin $ i*)
open Util
open Names
@@ -77,10 +77,46 @@ val force_entry_type :
val create_constr_entry :
string * gram_universe -> string -> constr_expr Gram.Entry.e
-val create_generic_entry : string -> ('a, constr_expr,raw_tactic_expr) abstract_argument_type -> 'a Gram.Entry.e
+val create_generic_entry : string -> ('a, rlevel,raw_tactic_expr) abstract_argument_type -> 'a Gram.Entry.e
val get_generic_entry : string -> grammar_object Gram.Entry.e
val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument_type
+(* Tactics as arguments *)
+
+val tactic_main_level : int
+
+val rawwit_tactic : int -> (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic : int -> (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic : int -> (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic0 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic0 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic0 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic1 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic1 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic1 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic2 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic2 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic2 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic3 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic3 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic3 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic4 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic4 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic4 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val rawwit_tactic5 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
+val globwit_tactic5 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
+val wit_tactic5 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+
+val is_tactic_genarg : argument_type -> bool
+
+val tactic_genarg_level : string -> int option
+
(* The main entry: reads an optional vernac command *)
val main_entry : (loc * vernac_expr) option Gram.Entry.e
@@ -148,7 +184,6 @@ module Tactic :
val simple_intropattern : Genarg.intro_pattern_expr Gram.Entry.e
val tactic_arg : raw_tactic_arg Gram.Entry.e
val tactic_expr : raw_tactic_expr Gram.Entry.e
- val tactic_main_level : int
val tactic : raw_tactic_expr Gram.Entry.e
val tactic_eoi : raw_tactic_expr Gram.Entry.e
end