Théophile Wallez

This issue looks similar to #2596, as noticed by @R1kM

I tested more thoroughly the parametrized `ring_mod` on my project, and noticed some times where the tactic is failing, for example: ```fstar let test_ring_cr3 (#m:nat{2 < m}) (a:mod_ring m) =...

The problem is that the tactic assume the ring is concrete so we can compute the result of operations between constants. The function `canonical_sum_simplify` generates conditions such as `if c...

One other solution would be to rewrite the `semiring_reflect` lemma: instead of the goal `interp_cs r vm (polynomial_simplify r e1) == interp_cs r vm (polynomial_simplify r e2)))`, we could write...

I don't intend to finish this pull request in the future, closing it.

I'm wondering if #2591 is related to this issue: the test there fails because F* tries to resolve tc2 before resolving tc1.

Now that I implemented the workaround in all my codebase, I can say it happens quite often. It make look similar to #2583, but #2583 only happened once (i.e. I...

Thank you for the interesting and detailed answer! My feeling was that since `?u1` is a `Q_Meta tcresolve` argument of `tc2`, then it could be instantiated with another invocation of...

@vapourismo Did you see that HACL* was already packaged with Nix? https://github.com/hacl-star/hacl-nix/blob/main/hacl/default.nix Other than that, I'm no Nix expert but I often saw fellow nixers advocating for `#!/usr/bin/env bash` instead...

This reminds me of #2245, I don't know if it is related.