aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Init/Logic.v
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2015-10-02 14:41:29 +0200
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2015-10-02 14:41:29 +0200
commit832ef36c5b066f5cb50a85b9a1450eaf7dcb9e44 (patch)
tree20093a471963d45b9d4913007c5e80c2f3c3be2b /theories/Init/Logic.v
parent9186689cbd5062a2535413369c72896e6f53a69b (diff)
emacs output mode: Added <infomsg> tag to debug messages.
So that they display in response buffer.
Diffstat (limited to 'theories/Init/Logic.v')
0 files changed, 0 insertions, 0 deletions