From 170da77ad45cb0e504f82d075836a8f2965efe28 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 20 Dec 2018 15:58:24 +0100
Subject: Documentation for SProp

---
 test-suite/success/sprop.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/success/sprop.v b/test-suite/success/sprop.v
index f2aba884d4..268c1880d2 100644
--- a/test-suite/success/sprop.v
+++ b/test-suite/success/sprop.v
@@ -24,7 +24,7 @@ Definition iSquash_rect A (P : iSquash A -> SProp) (H : forall x : A, P (isquash
 Fail Check (fun A : SProp => A : Type).
 
 Lemma foo : Prop.
-Proof. pose (fun A : SProp => A : Type). Abort.
+Proof. pose (fun A : SProp => A : Type); exact True. Fail Qed. Abort.
 
 (* define evar as product *)
 Check (fun (f:(_:SProp)) => f _).
@@ -186,4 +186,4 @@ Fail Definition relevance_unfixed := fun (A:SProp) (P:A -> Prop) x y (v:P x) =>
 
 (* 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).
+                                  ltac:(exact_no_check v) : P y.
-- 
cgit v1.2.3