diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-13 19:38:13 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-18 18:54:43 +0200 |
commit | 806e3bc0ecfbf0a6bfd20e80caa8250e60d39152 (patch) | |
tree | 21bda11bb7526d8dccc8c3883245ecf02762fc74 /toplevel/vernacentries.ml | |
parent | 575da16f72ac125ba7e50b1bfe63302dee639973 (diff) |
Print the type-in-type flag in various user-facing functions.
Diffstat (limited to 'toplevel/vernacentries.ml')
0 files changed, 0 insertions, 0 deletions