Commit 47f304f6 authored by Ralf Jung's avatar Ralf Jung

fix build with Coq 8.10 and newer

parent 1e481bde
......@@ -67,7 +67,7 @@ Canonical Structure namespace_mapC :=
Global Instance NamespaceMap_discrete a b :
Discrete a Discrete b Discrete (NamespaceMap a b).
Proof. by intros ?? [??] [??]; split; apply: discrete. Qed.
Proof. intros ?? [??] [??]; split; unfold_leibniz; by eapply discrete. Qed.
Global Instance namespace_map_ofe_discrete :
OfeDiscrete A OfeDiscrete namespace_mapC.
Proof. intros ? [??]; apply _. Qed.
......
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