Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

coqtop -quiet is less quiet in 8.14 than in 8.13 #15373

Open
andres-erbsen opened this issue Dec 16, 2021 · 0 comments
Open

coqtop -quiet is less quiet in 8.14 than in 8.13 #15373

andres-erbsen opened this issue Dec 16, 2021 · 0 comments
Labels
kind: regression Problems that were not present in previous versions. kind: user messages Improvement of error messages, new warnings, etc.

Comments

@andres-erbsen
Copy link
Contributor

andres-erbsen commented Dec 16, 2021

Description of the problem

$ /home/andreser/coq-8.13/bin/coqtop -quiet < /tmp/a.v 2>/dev/null
hi
$ /usr/bin/coqtop -quiet < /tmp/a.v 2>/dev/null                   
Welcome to Coq 8.14.1
[Loading ML file ring_plugin.cmxs ... done]
[Loading ML file zify_plugin.cmxs ... done]
[Loading ML file micromega_plugin.cmxs ... done]
1 goal
  
  ============================
  forall FOO : Prop, FOO
hi
$ cat /tmp/a.v                                 
Require Import Coq.ZArith.ZArith.
Goal forall FOO:Prop, FOO.
  idtac "hi".

Coq Version

8.14.1 vs 8.13.2

@andres-erbsen andres-erbsen added kind: user messages Improvement of error messages, new warnings, etc. kind: regression Problems that were not present in previous versions. labels Dec 16, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
kind: regression Problems that were not present in previous versions. kind: user messages Improvement of error messages, new warnings, etc.
Projects
None yet
Development

No branches or pull requests

1 participant