Commit a11f6dae authored by Glen Mével's avatar Glen Mével

Remove dependency on mathcomp, as ssreflect is now part of Coq 8.7.

parent a33e0491
From mathcomp Require Export ssreflect.
From Coq Require Export ssreflect.
From stdpp Require Export base list relations.
Tactic Notation "make_eq" constr(t) "as" ident(x) ident(E) :=
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment