aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/lemmas.ml
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-09-20 19:45:43 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-11-25 14:18:35 +0100
commit280c922fc55b57c430cad721c83650a796a375fd (patch)
tree5f0c9c20a75532ba134bbde6f428facefceb5125 /vernac/lemmas.ml
parentc93d5094bff73498ec8fc02837e16cc5ce9103b6 (diff)
Allow local universe renaming in Print.
Diffstat (limited to 'vernac/lemmas.ml')
0 files changed, 0 insertions, 0 deletions