diff options
Diffstat (limited to 'toplevel/vernacinterp.mli')
| -rw-r--r-- | toplevel/vernacinterp.mli | 41 |
1 files changed, 5 insertions, 36 deletions
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli index 2aa45f322..74f987ea4 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -9,47 +9,16 @@ (*i $Id$ i*) (*i*) -open Names -open Proof_type +open Tacexpr (*i*) -(* Interpretation of vernac phrases. *) +(* Interpretation of extended vernac phrases. *) -exception Drop -exception ProtectedLoop -exception Quit - val disable_drop : exn -> exn -type vernac_arg = - | VARG_VARGLIST of vernac_arg list - | VARG_STRING of string - | VARG_NUMBER of int - | VARG_NUMBERLIST of int list - | VARG_IDENTIFIER of identifier - | VARG_QUALID of Nametab.qualid - | VCALL of string * vernac_arg list - | VARG_CONSTR of Coqast.t - | VARG_CONSTRLIST of Coqast.t list - | VARG_TACTIC of Coqast.t - | VARG_TACTIC_ARG of tactic_arg - | VARG_BINDER of identifier list * Coqast.t - | VARG_BINDERLIST of (identifier list * Coqast.t) list - | VARG_AST of Coqast.t - | VARG_ASTLIST of Coqast.t list - | VARG_UNIT - | VARG_DYN of Dyn.t (* to put whatever you want *) - -val vinterp_add : string -> (vernac_arg list -> unit -> unit) -> unit +val vinterp_add : string -> (raw_generic_argument list -> unit -> unit) -> unit val overwriting_vinterp_add : - string -> (vernac_arg list -> unit -> unit) -> unit + string -> (raw_generic_argument list -> unit -> unit) -> unit -val vinterp_map : string -> vernac_arg list -> unit -> unit val vinterp_init : unit -> unit -val cvt_varg : Coqast.t -> vernac_arg -val call : string * vernac_arg list -> unit -val interp : Coqast.t -> unit - -(* raises an user error telling that the vernac command was called - with bad arguments *) -val bad_vernac_args : string -> 'a +val call : string * raw_generic_argument list -> unit |