Karl Palmskog

@maximedenes should I open a Coq issue about this (even though I don't know how to reproduce it without SerAPI)? Here is an extrapolation of the above example that still...

I think we at least figured out the overall circumstances for when this problem occurs and can work around it. Specifically, it's when a notation or tactic notation defines a...

As you suggested in #161, It may be easiest if I create a PR adding a test case using `sertok` on a `.v` file that includes the expected results and...

@brando90 I would suggest starting really minimalistically, e.g., a proof with 1-2 lines of proof scripts from [here](https://github.com/uwplse/StructTact/blob/master/Assoc.v) or [here](https://github.com/uwplse/StructTact/blob/master/Dedup.v). It may also help if you understand how multi-goal tactic...

I think it's fine if we merge `sercomp`/`compser`, as long as we can provide a simple mapping, e.g., `compser --mode=check f.sexp` is equivalent to `sercomp --input=sexp --output=check f.sexp`. Maybe we...

If I'm not mistaken, we are aiming to have four forms of input to `sercomp`: - regular vernacular (`.v` files): `vernac`(?) - sexp-serialized vernacular: `sexp`(?) - OCaml-serialized kernel terms +...

No matter how the roundtrip will work in the end, I think we can at least go ahead and add an option to `sercomp` to serialize environments, so our side...

This is a great start, but I will make some additions to the wish list of commands. In regression proving, we make a distinction between the digest/dependencies for the type...

I've given this some more thought now, and I believe we need kernel names (e.g., `mathcomp.ssreflect.fintype.uniq_enumP`) and not just digests for dependencies. Here is a revised proposal. Data structures: ```ocaml...

Here is an example to make things more concrete. ## Files in namespace `ST` `ListUtil.v`: ```coq Require Import List. Import ListNotations. Lemma remove_preserve : forall (A : Type) A_eq_dec (x...