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 (* TODO clashes with term below *)
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 ]
67 [ `Loc of location (* source file location *)
68 | `IdRef of string (* ACic pointer *)
72 | AttributedTerm of term_attribute * term
75 | Appl_symbol of string * int * term list (* literal, instance, args *)
76 | Binder of binder_kind * capture_variable * term (* kind, name, body *)
77 | Case of term * string * term option * (case_pattern * term) list
78 (* what to match, inductive type, out type, <pattern,action> list *)
79 | LetIn of capture_variable * term * term (* name, body, where *)
80 | LetRec of induction_kind * (capture_variable * term * int) list * term
81 (* (name, body, decreasing argument) list, where *)
82 | Ident of string * subst list (* literal, substitutions *)
83 | Meta of int * meta_subst list
84 | Num of string * int (* literal, instance *)
87 and capture_variable = Cic.name * term option (* name, type *)
88 and meta_subst = term option
89 and subst = string * term
90 and case_pattern = string * capture_variable list
94 | Symbol of string option * string * (subst option) * string option
95 (* h:xref, name, subst, definitionURL *)
96 | LocalVar of string option * string (* h:xref, name *)
97 | Meta of string option * string * meta_subst (* h:xref, name, meta_subst *)
98 | Num of string option * string (* h:xref, value *)
99 | Appl of string option * cexpr list (* h:xref, args *)
100 | Binder of string option *string * decl * cexpr
101 (* h:xref, name, decl, body *)
102 | Letin of string option * def * cexpr (* h:xref, def, body *)
103 | Letrec of string option * def list * cexpr (* h:xref, def list, body *)
104 | Case of string option * cexpr * ((string * cexpr) list)
105 (* h:xref, case_expr, named-pattern list *)
107 decl = string * cexpr (* name, type *)
109 def = string * cexpr (* name, body *)
111 subst = (UriManager.uri * cexpr) list
113 meta_subst = cexpr option list