blob: 77e8314d5fabea441af00856f2ec88471ccc909e (
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
|
(* $Id$ *)
open Term
type bindOcc =
| Dep of identifier
| NoDep of int
| Com
type 'a substitution = (bindOcc * 'a) list
type tactic_arg =
| COMMAND of Coqast.t
| CONSTR of constr
| IDENTIFIER of identifier
| INTEGER of int
| CLAUSE of identifier list
| BINDINGS of Coqast.t substitution
| CBINDINGS of constr substitution
| QUOTED_STRING of string
| TACEXP of Coqast.t
| REDEXP of string * Coqast.t list
| FIXEXP of identifier * int * Coqast.t
| COFIXEXP of identifier * Coqast.t
| LETPATTERNS of int list option * (identifier * int list) list
| INTROPATTERN of intro_pattern
and intro_pattern =
| IdPat of identifier
| DisjPat of intro_pattern list
| ConjPat of intro_pattern list
| ListPat of intro_pattern list
and tactic_expression = string * tactic_arg list
|
