Repair relevance marks in-kernel.

Prevent errors when under annotating binders.

1 files changed, 23 insertions, 0 deletions

diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v
index 995fd7eccc..f2aba884d4 100644
--- a/test-suite/success/sprop.v
+++ b/test-suite/success/sprop.v
@@ -2,6 +2,7 @@
 
 Set Primitive Projections.
 Set Warnings "+non-primitive-record".
+Set Warnings "+bad-relevance".
 
 Check SProp.
 
@@ -164,3 +165,25 @@ Section sFix.
     F x (fun (y:nat) (h: y < x) => sFix y (sAcc_inv x a y h)).
 
 End sFix.
+
+(** Relevance repairs *)
+
+Fail Definition fix_relevance : _ -> nat := fun _ : iUnit => 0.
+
+Require Import ssreflect.
+
+Goal forall T : SProp, T -> True.
+Proof.
+  move=> T +.
+  intros X;exact I.
+Qed.
+
+Set Warnings "-bad-relevance".
+Definition fix_relevance : _ -> nat := fun _ : iUnit => 0.
+
+(* relevance isn't fixed when checking P x == P y *)
+Fail Definition relevance_unfixed := fun (A:SProp) (P:A -> Prop) x y (v:P x) => v : P y.
+
+(* but the kernel is fine *)
+Definition relevance_unfixed := fun (A:SProp) (P:A -> Prop) x y (v:P x) =>
+                                  ltac:(refine (_:P y);exact_no_check v).