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 ]
63 type induction_kind = [ `Inductive | `CoInductive ]
64 type sort_kind = [ `Prop | `Set | `Type | `CProp ]
66 type case_pattern = string list
69 | LocatedTerm of location * term
72 | Appl_symbol of string * int * term list (* literal, args, instance *)
73 | Binder of binder_kind * Cic.name * term option * term
74 (* kind, name, type, body *)
75 | Case of term * string * term option * (case_pattern * term) list
76 (* what to match, inductive type, out type, <pattern,action> list *)
77 | LetIn of string * term * term (* name, body, where *)
78 | LetRec of induction_kind * (string * term * term option * int) list * term
79 (* (name, body, type, decreasing argument) list, where *)
80 | Ident of string * subst list (* literal, substitutions *)
81 | Meta of int * meta_subst list
82 | Num of string * int (* literal, instance *)
85 and meta_subst = term option
86 and subst = string * term
90 | Symbol of string option * string * (subst option) * string option
91 (* h:xref, name, subst, definitionURL *)
92 | LocalVar of string option * string (* h:xref, name *)
93 | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *)
94 | Num of string option * string (* h:xref, value *)
95 | Appl of string option * cexpr list (* h:xref, args *)
96 | Binder of string option *string * decl * cexpr
97 (* h:xref, name, decl, body *)
98 | Letin of string option * def * cexpr (* h:xref, def, body *)
99 | Letrec of string option * def list * cexpr (* h:xref, def list, body *)
100 | Case of string option * cexpr * ((string * cexpr) list)
101 (* h:xref, case_expr, named-pattern list *)
103 decl = string * cexpr (* name, type *)
105 def = string * cexpr (* name, body *)
107 subst = (UriManager.uri * cexpr) list
109 meta_subst = cexpr option list