aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/lemmas.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-09-10 02:21:03 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-09-28 16:51:21 +0200
commitb772c323f62b322c9b0a4ab90c7de8b1e2066bae (patch)
tree16dc8bc2ae1b5374a1329b9f6495d0a1b9905ee4 /vernac/lemmas.ml
parentd28304f6ba18ad9527a63cd01b39a5ad27526845 (diff)
Efficient computation of the names contained in an environment.
Diffstat (limited to 'vernac/lemmas.ml')
0 files changed, 0 insertions, 0 deletions