Filter to actually unsatisfied constraint in error message

Maybe we should be filtering when raising instead?

Or instead of doing

~~~
if not @@ check_constraints csts
then error_unsat_constraint csts
~~~

we should do

~~~
Constraints.iter (fun cst ->
  if not @@ check_constraint cst
  then error_unsat_constraint csts)
  csts
~~~
? although then we would only mention the first unsatisfied constraint.

test-suite/output/unsat_constraints.out

@@ -0,0 +1,4 @@
+File "./output/unsat_constraints.v", line 22, characters 2-15:
+The command has indeed failed with message:
+Unsatisfied constraints: v < w
+                         u <= w (maybe a bugged tactic).

test-suite/output/unsat_constraints.v

@@ -0,0 +1,23 @@
+Require Import Ltac2.Ltac2.
+
+Import Constr.
+Import Unsafe.
+
+Polymorphic Axiom foo@{u v w | u < v, u <= w, v < w} : Prop.
+
+Polymorphic Axiom bar@{u v w | } : Prop.
+
+Universes u v w.
+
+Constraint u < v.
+
+Lemma baz : Prop.
+Proof.
+  (* easiest way to get unsatisfied constraints *)
+  match kind 'bar@{u v w}, kind 'foo  with
+  | Constant _ u, Constant c _ => Std.exact_no_check (make (Constant c u))
+  | _ => Control.throw Assertion_failure
+  end.
+  (* should mention u <= w and v < w but not u < v *)
+  Fail Defined.
+Abort.

vernac/himsg.ml

@@ -794,6 +794,7 @@ let explain_non_linear_unification env sigma m t =
   pr_leconstr_env env sigma t ++ str "."
 
 let explain_unsatisfied_constraints env sigma cst =
+  let cst = Univ.Constraints.filter (fun cst -> not @@ UGraph.check_constraint (Evd.universes sigma) cst) cst in
   strbrk "Unsatisfied constraints: " ++
     Univ.Constraints.pr (Termops.pr_evd_level sigma) cst ++
     spc () ++ str "(maybe a bugged tactic)."