X-Git-Url: http://git.megacz.com/?p=coq-hetmet.git;a=blobdiff_plain;f=src%2FReificationFromGeneralizedArrow.v;fp=src%2FReificationFromGeneralizedArrow.v;h=1a5fea717e0bf95febb636aa4b1fe0283fe06f63;hp=2a9937f52ea5f655d2dc6b8a06e4a832a387cf40;hb=77e8c70f4fd7a32db036fee5884a98208d450de2;hpb=64d416692bda1d36c33b5efa245d46dcf546ad4a

diff --git a/src/ReificationFromGeneralizedArrow.v b/src/ReificationFromGeneralizedArrow.v
index 2a9937f..1a5fea7 100644
--- a/src/ReificationFromGeneralizedArrow.v
+++ b/src/ReificationFromGeneralizedArrow.v
@@ -34,6 +34,7 @@ Definition reification_from_garrow (K:Enrichment) {ce} (C:MonoidalEnrichment ce)
    ; reification_rstar     := PreMonoidalFunctorsCompose garrow C
    |}.
    abstract (intros; set (@ni_associativity) as q; apply q).
+   intros; apply ga_host_lang_pure.
    Defined.