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 945209d commit 8dace80Copy full SHA for 8dace80
_CoqProject.test-suite
@@ -53,6 +53,7 @@ examples/Coq2020_material/CoqWS_expansion/withHB.v
53
examples/Coq2020_material/CoqWS_expansion/withoutHB.v
54
55
examples/cat/cat.v
56
+tests/enriched_cat_case6.v
57
58
tests/type_of_exported_ops.v
59
tests/duplicate_structure.v
tests/enriched_cat_case6.v
@@ -467,6 +467,7 @@ eapply functional_extensionality; intro x0.
467
refine (mrid _).
468
Qed.
469
470
+stop
471
472
Program Definition icmfunQ_isICAlg (A B: ICMon.type) :
473
isICAlg (hom A B) := isICAlg.Build (hom A B) _ _.
0 commit comments