diff options
| author | Matthieu Sozeau | 2016-05-20 03:18:41 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-16 18:21:08 +0200 |
| commit | 677d5deb72734a0e5502bcf47a905fcdf9374e51 (patch) | |
| tree | c8812b98a4c5c2f34412b5d39a054be474679457 /kernel/type_errors.mli | |
| parent | 8d06718fd4d99f4e5bc33452a02ea27d5a9279ed (diff) | |
Proofview: extensions for backtracking eauto
unshelve_goals is used to correctly register dependent
subgoals that have to be solved. Resolution may fail to
do so using hints, so we have to put them back as goals
in that case. The shelf is a good interface for doing that.
unifiable can be used outside proofview to detect dependencies
between goals. This might be better in another module.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions