Pierre Villemot

As I expected, we got regressions if we do not produce a context in the `make` function of `Adt` as we did in `Records`. Consider for instance this example (I...

In the last patch, I use the context of `Adt.make` to propagate the same equalities as we did in `Records.make`. Actually I produce these equalities as soon as the type...

+55-12 on ae-format and the solver is slightly faster :)

Okay, I was not completely satisfied by the last commit. It is sad to still use the context of `X.make`. Another way to solve this issue consists in eliminating as...

I think that this PR is now ready to review. I keep the current code with context in `X.make` even if I dislike this design because I didn't find a...

> I am really uneasy about losing such simple proofs as the 1008 example — we really should figure out a way to send those terms back to matching. I...

Ok, this PR is quite old... I thought `1008/record.smt2` was a regression but it wasn't! Before this PR, we cannot prove the test with both `Tableaux` and `CDCL`. After this...

After a quick investigation, I have an almost correct patch to apply on `uf.ml`: ```patch diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 4049634c..391c3746 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1122,14 +1122,19 @@...

I caught the bug because I ran model tests with both CDCL-Tableaux and CDCL. I didn't intend to test the feature with CDCL but it happened when I modified `gentest`....

I added a prototype for a wiki syntax checker in `test/` directory. You can run it as follows: ``` dune exec -- test/wiki_check.exe --bd base_directory bname ``` where `bname` is...