aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/tacsubst.mli
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-04-24 14:07:39 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-04-29 13:41:24 +0200
commit080c5fd2a6cbf390172e086b594b0bd649aa118b (patch)
tree800434b5daa19e27aedfae38ca2950005018af95 /plugins/ltac/tacsubst.mli
parentf54cbf01ad2aab14eed671e02b98f6962b05a38d (diff)
Implement to_constr with nf_evars_and_universes_opt_subst
Diffstat (limited to 'plugins/ltac/tacsubst.mli')
0 files changed, 0 insertions, 0 deletions