blob: 5f302f1b9a090305188782f2902cc08381e60d2a (
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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Pp
open Names
open Proof_type
open Tacmach
open Tactic_debug
open Term
open Tacexpr
open Genarg
open Constrexpr
open Mod_subst
open Redexpr
open Misctypes
open Nametab
(** Globalization of tactic expressions :
Conversion from [raw_tactic_expr] to [glob_tactic_expr] *)
type glob_sign = {
ltacvars : Id.t list * Id.t list;
ltacrecvars : (Id.t * ltac_constant) list;
gsigma : Evd.evar_map;
genv : Environ.env }
val fully_empty_glob_sign : glob_sign
val make_empty_glob_sign : unit -> glob_sign
(** same as [fully_empty_glob_sign], but with [Global.env()] as
environment *)
(** Main globalization functions *)
val glob_tactic : raw_tactic_expr -> glob_tactic_expr
val glob_tactic_env :
Id.t list -> Environ.env -> raw_tactic_expr -> glob_tactic_expr
(** Low-level variants *)
val intern_pure_tactic : glob_sign -> raw_tactic_expr -> glob_tactic_expr
val intern_tactic_or_tacarg :
glob_sign -> raw_tactic_expr -> Tacexpr.glob_tactic_expr
val intern_constr : glob_sign -> constr_expr -> glob_constr_and_expr
val intern_constr_with_bindings :
glob_sign -> constr_expr * constr_expr bindings ->
glob_constr_and_expr * glob_constr_and_expr bindings
val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located
(** Adds a globalization function for extra generic arguments *)
type intern_genarg_type =
glob_sign -> raw_generic_argument -> glob_generic_argument
val add_intern_genarg : string -> intern_genarg_type -> unit
val intern_genarg : intern_genarg_type
(** Adds a definition of tactics in the table *)
val add_tacdef :
Vernacexpr.locality_flag -> bool ->
(Libnames.reference * bool * raw_tactic_expr) list -> unit
val add_primitive_tactic : string -> glob_tactic_expr -> unit
(** Tactic extensions *)
val add_tactic :
string -> (typed_generic_argument list -> tactic) -> unit
val overwriting_add_tactic :
string -> (typed_generic_argument list -> tactic) -> unit
val lookup_tactic :
string -> (typed_generic_argument list) -> tactic
val lookup_ltacref : ltac_constant -> glob_tactic_expr
(** printing *)
val print_ltac : Libnames.qualid -> std_ppcmds
(** Reduction expressions *)
val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr
val dump_glob_red_expr : raw_red_expr -> unit
|
