1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: proof_type.ml 12168 2009-06-06 21:34:37Z herbelin $ *)
26
(* This module defines the structure of proof tree and the tactic type. So, it
27
is used by Proof_tree and Refiner *)
31
| Cut of bool * bool * identifier * types
32
| FixRule of identifier * int * (identifier * int * constr) list * int
33
| Cofix of identifier * (identifier * constr) list * int
35
| Convert_concl of types * cast_kind
36
| Convert_hyp of named_declaration
37
| Thin of identifier list
38
| ThinBody of identifier list
39
| Move of bool * identifier * identifier move_location
40
| Order of identifier list
41
| Rename of identifier * identifier
47
ref : (rule * proof_tree list) option }
51
| Nested of compound_rule * proof_tree
56
| Tactic of tactic_expr * bool
57
| Proof_instr of bool*proof_instr (* the boolean is for focus restrictions *)
61
and tactic = goal sigma -> (goal list sigma * validation)
63
and validation = (proof_tree list -> proof_tree)
68
evaluable_global_reference,
73
Tacexpr.gen_tactic_expr
75
and atomic_tactic_expr =
78
evaluable_global_reference,
83
Tacexpr.gen_atomic_tactic_expr
88
evaluable_global_reference,
93
Tacexpr.gen_tactic_arg
95
type hyp_location = identifier Tacexpr.raw_hyp_location
98
| LtacNotationCall of string
99
| LtacNameCall of ltac_constant
100
| LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
101
| LtacVarCall of identifier * glob_tactic_expr
102
| LtacConstrInterp of rawconstr *
103
((identifier * constr) list * (identifier * identifier option) list)
105
type ltac_trace = (loc * ltac_call_kind) list
107
exception LtacLocated of (ltac_call_kind * ltac_trace * loc) * exn
109
let abstract_tactic_box = ref (ref None)