change `contra_not` when requiring MathComp > 1.14 #667

Closed

Milestone

opened

analysis/theories/topology.v

Line 3181 in 6b30ce5

    
           have := @contra_not _ _ (T_filterT2 x y); rewrite (rwP eqP) (rwP negP).  (* change @contra_not _ _ to contra_not when requiring MathComp > 1.14 *)

Metadata

Assignees

No one assigned

Labels

No labels

No labels

Type

No type

Projects

No projects

Milestone

0.6.7

Relationships

None yet

Development

No branches or pull requests