aboutsummaryrefslogtreecommitdiff
path: root/lib/objFile.ml
diff options
context:
space:
mode:
authorJim Fehrle2020-10-11 19:15:51 -0700
committerJim Fehrle2020-10-27 12:17:21 -0700
commitede77b72328c98995c0636656bb71ba87861ddfe (patch)
tree69510ffd33c71a461b22dea76d42656bf4d3293d /lib/objFile.ml
parentb402adc12c00ba72046423d3a1737ccad517f70e (diff)
Rename tactic_expr -> ltac_expr
Diffstat (limited to 'lib/objFile.ml')
0 files changed, 0 insertions, 0 deletions