diff options
| author | Pierre-Marie Pédrot | 2014-05-23 18:41:47 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-06-03 01:20:36 +0200 |
| commit | 259ec71685cf2180403e35acea32cb42ba6b761b (patch) | |
| tree | 20364037953979d99e722591d2445fe5aa144b78 /kernel/type_errors.mli | |
| parent | 2e3f59f8d689b45fcad8cfd0f3dc1d5e693d8546 (diff) | |
The tactic interpreter now uses a new type of tactics, through
the GTac module. A ['a Gtac.t] is a special case of tactic that
may depend on the current goals, or not. Internally, it construct
a list of results, one for each focussed goal, if the tactic is
actually dependent.
This allows for an interpretation of whole-goal tactic that does
work, which was not the case for the previous implementation,
which did to many Proofview.Goal.enter.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions