diff options
| author | Arnaud Spiwack | 2014-02-27 11:46:43 +0100 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-02-27 11:46:43 +0100 |
| commit | 0a1c88bb9400cb16c3dba827e641086215497e8c (patch) | |
| tree | 9f91f8c2b70cb3ae659be484ae881b244ce43d89 /kernel/nativecode.ml | |
| parent | b1ebce6e811eb6e1d4476b873e13155cc83c5ee1 (diff) | |
Get rid of the enterl/glist API for Proofview.Goal.
The prefered style is to use continuation passing style when necessary, or simply passing the goal explicitely in the case of interpretation functions which do not evolve the current goal.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions