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.mli 12168 2009-06-06 21:34:37Z herbelin $ i*)
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
44
(* The type [goal sigma] is the type of subgoal. It has the following form
46
it = { evar_concl = [the conclusion of the subgoal]
47
evar_hyps = [the hypotheses of the subgoal]
48
evar_body = Evar_Empty;
49
evar_info = { pgm : [The Realizer pgm if any]
50
lc : [Set of evar num occurring in subgoal] }}
51
sigma = { stamp = [an int chardacterizing the ed field, for quick compare]
52
ed : [A set of existential variables depending in the subgoal]
54
it = { evar_concl = [the type of first evar]
55
evar_hyps = [the context of the evar]
56
evar_body = [the body of the Evar if any]
57
evar_info = { pgm : [Useless ??]
58
lc : [Set of evars occurring
59
in the type of evar] } };
62
it = { evar_concl = [the type of evar]
63
evar_hyps = [the context of the evar]
64
evar_body = [the body of the Evar if any]
65
evar_info = { pgm : [Useless ??]
66
lc : [Set of evars occurring
67
in the type of evar] } } }
73
[ref] = [None] if the goal has still to be proved,
74
and [Some (r,l)] if the rule [r] was applied to the goal
75
and gave [l] as subproofs to be completed.
76
if [ref = (Some(Nested(Tactic t,p),l))] then [p] is the proof
77
that the goal can be proven if the goals in [l] are solved. *)
81
ref : (rule * proof_tree list) option }
85
| Nested of compound_rule * proof_tree
90
(* the boolean of Tactic tells if the default tactic is used *)
91
| Tactic of tactic_expr * bool
92
| Proof_instr of bool * proof_instr
96
and tactic = goal sigma -> (goal list sigma * validation)
98
and validation = (proof_tree list -> proof_tree)
103
evaluable_global_reference,
108
Tacexpr.gen_tactic_expr
110
and atomic_tactic_expr =
113
evaluable_global_reference,
118
Tacexpr.gen_atomic_tactic_expr
123
evaluable_global_reference,
128
Tacexpr.gen_tactic_arg
130
type hyp_location = identifier Tacexpr.raw_hyp_location
132
type ltac_call_kind =
133
| LtacNotationCall of string
134
| LtacNameCall of ltac_constant
135
| LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
136
| LtacVarCall of identifier * glob_tactic_expr
137
| LtacConstrInterp of rawconstr *
138
((identifier * constr) list * (identifier * identifier option) list)
140
type ltac_trace = (loc * ltac_call_kind) list
142
exception LtacLocated of (ltac_call_kind * ltac_trace * loc) * exn
144
val abstract_tactic_box : atomic_tactic_expr option ref ref