aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/tacenv.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-11-06 21:59:18 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-02-14 17:26:38 +0100
commitb77579ac873975a15978c5a4ecf312d577746d26 (patch)
tree772e41667e74c38582ff6f4645c73e7d7556f935 /ltac/tacenv.mli
parent258c8502eafd3e078a5c7478a452432b5c046f71 (diff)
Tacred API using EConstr.
Diffstat (limited to 'ltac/tacenv.mli')
0 files changed, 0 insertions, 0 deletions