2 (* when an 'ident option is None, the default is to apply the tactic
5 type reduction_kind = [ `Reduce | `Simpl | `Whd ]
10 type location = int * int
12 type ('term, 'ident) tactic =
13 | LocatedTactic of location * ('term, 'ident) tactic
18 | Change of 'term * 'term * 'ident option (* what, with what, where *)
19 | Change_pattern of 'term pattern * 'term * 'ident option
20 (* what, with what, where *)
23 | Decompose of 'ident * 'ident list (* which hypothesis, which principles *)
24 | Discriminate of 'ident
25 | Elim of 'term * 'term option (* what to elim, which principle to use *)
29 | Fold of reduction_kind * 'term
32 | Intros of int option
34 | LetIn of 'term * 'ident
35 | Named_intros of 'ident list
36 | Reduce of reduction_kind * 'term pattern * 'ident option (* what, where *)
38 | Replace of 'term * 'term (* what, with what *)
39 | Replace_pattern of 'term pattern * 'term
40 | RewriteLeft of 'term * 'ident option
41 | RewriteRight of 'term * 'ident option
46 | Transitivity of 'term
48 type 'tactic tactical =
49 | LocatedTactical of location * 'tactic tactical
52 | For of int * 'tactic tactical
54 | Repeat of 'tactic tactical
55 | Seq of 'tactic tactical list (* sequential composition *)
57 | Then of 'tactic tactical * 'tactic tactical list
58 | Tries of 'tactic tactical list
59 (* try a sequence of tacticals until one succeeds, fail otherwise *)
60 | Try of 'tactic tactical (* try a tactical and mask failures *)
62 type binder_kind = [ `Lambda | `Pi | `Exists | `Forall ]
64 type case_pattern = string list
67 | LocatedTerm of location * term
70 | Binder of binder_kind * string * term option * term
71 (* kind, name, type, body *)
72 | Case of term * term option * (case_pattern * term) list
73 (* what to match, case type, <pattern,action> list *)
74 | LetIn of string * term * term (* name, body, where *)
75 | LetRec of (string * term * term option * int) list * term
76 (* (name, body, type, decreasing argument) list, where *)
77 | Ident of string * subst list
78 | Meta of string * meta_subst list
81 and meta_subst = term option
82 and subst = string * term
86 | Symbol of string option * string * (subst option) * string option
87 (* h:xref, name, subst, definitionURL *)
88 | LocalVar of string option * string (* h:xref, name *)
89 | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *)
90 | Num of string option * string (* h:xref, value *)
91 | Appl of string option * cexpr list (* h:xref, args *)
92 | Binder of string option *string * decl * cexpr
93 (* h:xref, name, decl, body *)
94 | Letin of string option * def * cexpr (* h:xref, def, body *)
95 | Letrec of string option * def list * cexpr (* h:xref, def list, body *)
96 | Case of string option * cexpr * ((string * cexpr) list)
97 (* h:xref, case_expr, named-pattern list *)
99 decl = string * cexpr (* name, type *)
101 def = string * cexpr (* name, body *)
103 subst = (UriManager.uri * cexpr) list
105 meta_subst = cexpr option list