aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/g_ground.ml4
diff options
context:
space:
mode:
authorGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-02-27 11:46:43 +0100
committerGravatar Arnaud Spiwack <arnaud@spiwack.net>2014-02-27 11:46:43 +0100
commit0a1c88bb9400cb16c3dba827e641086215497e8c (patch)
tree9f91f8c2b70cb3ae659be484ae881b244ce43d89 /plugins/firstorder/g_ground.ml4
parentb1ebce6e811eb6e1d4476b873e13155cc83c5ee1 (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 'plugins/firstorder/g_ground.ml4')
0 files changed, 0 insertions, 0 deletions