We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 8a5f377 commit 6f62e00Copy full SHA for 6f62e00
HB/structures.v
@@ -1,5 +1,5 @@
1
(* Support constants, to be kept in sync with shim/structures.v *)
2
-From Coq Require Import ssreflect ssrfun.
+From Corelib Require Import ssreflect ssrfun.
3
4
Variant error_msg := NoMsg | IsNotCanonicallyA (x : Type).
5
Definition unify T1 T2 (t1 : T1) (t2 : T2) (s : error_msg) :=
0 commit comments