aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind/indfun.ml
diff options
context:
space:
mode:
authorGaƫtan Gilbert2019-05-20 17:08:38 +0200
committerEnrico Tassi2019-06-04 13:58:42 +0200
commit1ea1e218eed9792685bd7467b63a17fb5ebdbb7e (patch)
tree9bf108186e892513ac4a949a3b6ddf31c05ef328 /plugins/funind/indfun.ml
parent788b47d9dd70dc9f8057d4a9353ed24f091ea917 (diff)
Rename Proof_global.{t -> stack}
Diffstat (limited to 'plugins/funind/indfun.ml')
0 files changed, 0 insertions, 0 deletions