Georges Gonthier

As it stands, part of the change is not backward compatible : adding the new `[in A]` notation obviously is, but using it in the `[predU A & B]`, `[predI...

Indeed, I do confirm that this is now purely a uniform inheritance issue. As documented in detail in `ssrbool`, it is necessary for the `topred` projection of `predType`s to be...

@amahboubi this can definitely wait for a future version, but is something we should eventually do - hence the issue.

I was mostly getting rid of negative selectors, and in a few cases having some form of negative pattern would have made it easier to avoid the `set; rewrite [..]/..`...

The have should fail, because you are allowed only a single intro pattern (with clear & views before and simpl switches after) in a have, as additional identifiers are interpreted...

@gares "day one" is a bit of an overstatement - this did use to work as intended in the original version of the code...

I think the debug value is just as good for indexes as it is for main terms, so there's no compelling reason for introducing an inconsistency here. It's not unlikely...

These definitions were left undocumented because they are all considered to be internal: - `grepr0`, `dadd_grepr`, `muln_grepr` are essentially only used to construct `standard_grepr` - Indeed the `representation` type which...

This is a known issue, and essentially a Coq one, so if you want to draw attention to it you you also raise it over there. Essentially here the `SSReflect`...

Using `Hint Extern` is an acceptable local fix, but it has to be used sparingly for global hints to avoid undue performance degradation. Having a variant of `trivial` that matches...