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 d8d51ca commit 476636cCopy full SHA for 476636c
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