Ssreflect Users Discussion List

[Robbert Krebbers <>]

Hi list,

I'm looking into using ssreflect, and in particular the rewrite tactic 
for its better sub-term selection and compactness, for one of my Coq 
developments. While doing partially automated proofs, I often make use 
of "rewrite foo in hyp", which does not work well in ssreflect: it 
changes the order of the hypotheses, and it does not work with setoids. 
See the attached example.

I am using Coq 8.5rc1 and the most recent ssr from git.

Best,

Robbert

Attachment: 20160113_ssr_rewrite_in_hyp.v
Description: application/extension-v