MetaCoq: TemplateProgram: Going to run (Core.tmReturn@{Common.option_instance.u0
                                          WithTemplate.tmRetypeAroundMetaCoqBug853.u1}
                                          (Common.my_Value@{Common.option_instance.u0}
                                             {|
                                               Common.my_projT1 :=
                                                 quotation_of
                                                   KernameSetOrdProp.ME.OrderTac.TO.t;
                                               Common.my_projT2 :=
                                                 Ast.tConst
                                                   (MPdot
                                                      (MPdot
                                                      (MPdot
                                                      (MPdot
                                                      (MPfile
                                                      ["Kernames"%bs; "Common"%bs;
                                                      "MetaCoq"%bs])
                                                      "KernameSetOrdProp"%bs)
                                                      "ME"%bs) "OrderTac"%bs)
                                                      "TO"%bs, "t"%bs)
                                                   ([] : Universes.Instance.t)
                                             |}))</infomsg>
Toplevel input, characters 0-77:
> MetaCoq Run (tmMakeQuotationOfModule everything None "KernameSetOrdProp.ME").
> ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: Conversion test raised an anomaly:
Anomaly
"in Univ.repr: Universe MetaCoq.Quotation.ToTemplate.QuotationOf.Common.Kernames.KernameSetOrdProp.Instances.13 undefined."
Please report at http://coq.inria.fr/bugs/.