From 2209e0bce7eeda751f87806a3e77a0c520017a88 Mon Sep 17 00:00:00 2001
From: Enrico
Date: Wed, 7 Sep 2016 18:02:09 +0200
Subject: fix comment

---
 mathcomp/ssreflect/ssreflect.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/ssreflect.v b/mathcomp/ssreflect/ssreflect.v
index 6750142..cd405fa 100644
--- a/mathcomp/ssreflect/ssreflect.v
+++ b/mathcomp/ssreflect/ssreflect.v
@@ -426,7 +426,8 @@ Hint View for apply/ iffRLn|2 iffLRn|2 iffRL|2 iffLR|2.
 (* Usage:                                                      *)
 (*   elim/abstract_context: (pattern) => G defG.               *)
 (*   vm_compute; rewrite {}defG {G}.                           *)
-(* Note that vm_cast are not stored in the proof term, so      *)
+(* Note that vm_cast are not stored in the proof term          *)
+(* for reductions occuring in the context, hence               *)
 (*   set here := pattern; vm_compute in (value of here)        *)
 (* blows up at Qed time.                                       *)
 Lemma abstract_context T (P : T -> Type) x :
-- 
cgit v1.2.3