aboutsummaryrefslogtreecommitdiff
path: root/vernac/comProgramFixpoint.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2018-04-26 14:49:08 +0200
committerGaëtan Gilbert2018-05-14 13:25:56 +0200
commite68f8c904b7ee8fee9f98f75e37ab6d01b54731f (patch)
treebea31974cad014170e42f0bb87ac2163500092c9 /vernac/comProgramFixpoint.ml
parent5b432bf03f623b144871181446c68479482abe32 (diff)
Typing: define functional alternatives to e_* functions
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
0 files changed, 0 insertions, 0 deletions