aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.mli
diff options
context:
space:
mode:
authorGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2015-10-02 14:41:57 +0200
committerGravatar Pierre Courtieu <Pierre.Courtieu@cnam.fr>2015-10-02 14:41:57 +0200
commit88abc50ece70405d71777d5350ca2fa70c1ff437 (patch)
treea290d8f8cb67f0e337a23d71cbb308d444adaf10 /pretyping/evarconv.mli
parent832ef36c5b066f5cb50a85b9a1450eaf7dcb9e44 (diff)
Changed status of Info messages from notice to info.
This fixes a bug in proofgeneral. PG will now diplay this message eagerly. Otherwise since they appear before the goal, they are considered outdated and not displayed.
Diffstat (limited to 'pretyping/evarconv.mli')
0 files changed, 0 insertions, 0 deletions