diff options
| author | Enrico | 2016-09-07 18:02:09 +0200 |
|---|---|---|
| committer | GitHub | 2016-09-07 18:02:09 +0200 |
| commit | 2209e0bce7eeda751f87806a3e77a0c520017a88 (patch) | |
| tree | 825eb73d3394e545c7a0aacd22de77aea658ce64 /mathcomp/ssreflect | |
| parent | 806b05dc5c3a1594231225df0e8e9e28441d8736 (diff) | |
fix comment
Diffstat (limited to 'mathcomp/ssreflect')
| -rw-r--r-- | mathcomp/ssreflect/ssreflect.v | 3 |
1 files changed, 2 insertions, 1 deletions
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 : |