aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/elim.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-07 18:02:52 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-09-08 15:52:56 +0200
commitdfac5aa2285de5b89f08ada3c30c0a1594737440 (patch)
tree37fa3f3481d03c4a777595e1ec0eab631cd528aa /tactics/elim.mli
parent13266ce4c37cb648b5e4e391aa5d7486bbcdb4ee (diff)
Making Vernacexpr independent from Tacexpr.
Diffstat (limited to 'tactics/elim.mli')
0 files changed, 0 insertions, 0 deletions