Error compiling the updated HoTT library

[Kristina Sojakova]

Dear all,

I get the following error when trying to compile the new HoTT library:

File "/home/kristina/HoTT/theories/hit/epi.v", line 4, characters 0-65:
Anomaly: Mismatched instance and context when building universe substitution.
Please report.

I have the latest version of Coq (from the trunk).

Thanks,

Kristina

[Bas Spitters]

It is likely to be due to one of Matthieu's latest commits from April 17th.
https://github.com/HoTT/coq/commits/trunk

The version from April 9th still works for me.
Sorry, I do not have more time to test now.

> --
> You received this message because you are subscribed to the Google Groups
> "IAS Univalent Foundations" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to univalent-founda...@googlegroups.com.
> To post to this group, send email to univalent-...@googlegroups.com.
> Visit this group at
> http://groups.google.com/group/univalent-foundations?hl=en.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>