blob: aa71f411dc71c75dff9e45e1d9e98e331bc36394 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
(* $Id$ *)
(*i*)
open Pp
open Names
open Proof_trees
open Tacmach
open Term
(*i*)
(* Interpretation of tactics. *)
val cvt_arg : Coqast.t -> tactic_arg
val tacinterp_add : string * (tactic_arg list -> tactic) -> unit
val tacinterp_map : string -> tactic_arg list -> tactic
val tacinterp_init : unit -> unit
val interp : Coqast.t -> tactic
val interp_atomic : Coqast.loc -> string -> tactic_arg list -> tactic
val interp_semi_list : tactic -> Coqast.t list -> tactic
val vernac_interp : Coqast.t -> tactic
val vernac_interp_atomic : identifier -> tactic_arg list -> tactic
val overwriting_tacinterp_add : string * (tactic_arg list -> tactic) -> unit
val is_just_undef_macro : Coqast.t -> string option
|
