-
Notifications
You must be signed in to change notification settings - Fork 0
Home
For the moment, the development branch is gmalecha/coq-8.6. It is against this one that PR have to be done.
Description of the other branches:
-
mattam82/typing: Experiments about implementing a Coq type checker in Coq.
-
aa755/cast86 : This version contains a monad for programming with template-coq operations. It also provides a lossless way of reifiying inductives (https://github.com/gmalecha/template-coq/issues/17). Unfortunately, there is some small extra code to put a cast (:Set) around types of type Set. I will soon remove that part in a different branch.
-
aa755/castTrunk : In addition to the above, this fork includes support of universe levels, as implemented by @yforster. This version used to compile with trunk at the end of Coq Implementor's workshop. After cumulativity of inductives were added, something broke.
-
SimonBoulier/holes Experiments with holes