Qinshi Wang

Is VST sound for traceless infinite loops? It's said loops like `for (;;)` can be assumed to terminate. [infinite loop ](https://stackoverflow.com/questions/15595493/is-an-empty-infinite-loop-undefined-behavior-in-c)

It seems `> Coq: Print Implicit Arguments` does not work properly. It should do `Set Printing Implicit` like CoqIDE, but it happens to open a menu.

@TheoWinterhalter Thanks for your reply. But implicit arguments refer to [link](https://coq.inria.fr/refman/language/extensions/implicit-arguments.html) (or [link](https://coq.inria.fr/refman/language/extensions/implicit-arguments.html#implicit-argument-binders) for examples). In CoqIDE, `Display Implicit Arguments` means to only display these implicit arguments, but not notations,...

@fakusb It seems also to do nothing for me. I am using VSCoq 0.3.2 from VS Code extension market.

`sep_apply` has special manipulation for assumptions in the form of `!! ?P && _` (see [here](https://github.com/PrincetonUniversity/VST/blob/master/floyd/seplog_tactics.v#L1103)). So for `(!!P && B) |-- C`, `sep_apply` treats it as `P -> B...

I encountered this issue again recently and was able to figure out a small example. ```coq Require Import Coq.Lists.List. Require Import Hammer.Plugin.Hammer. Import ListNotations. Class ExternSem := { extern_state :...

In my opinion, it is a real bug rather than a documentation issue. We expect `eauto` as matching the head symbol and try `simple eapply`. It's very confusing if `simple...

`make` is making from source code, not from OPAM.

Maybe I wrote this part of the code, but I cannot remember everything. `ecareful_unify` looks weaker than `unify` and do less evar instantiation. You want to unify `if ?a then...

I hope to have [VST zlist](https://github.com/PrincetonUniversity/VST/blob/master/coq-vst-zlist.opam) as an explicitly included package in the next Coq Platform. VST zlist is always included in any VST installation, but having it explicitly mentioned...