0aca9f2New module chaser, for better dependency checking and rebuilding Now treats each source file separately, building a tree of dependencies, and rebuilding if any dependencies have updated. In particular, this fixes a problem with stale definitions hanging around when building packages, and has required some fixes to imports in the library.Edwin Brady13 years ago e002347change traverse on Binder to a Traversable instanceMelvar Chen13 years ago ee06705rename fmap to mapMelvar Chen13 years ago 7fc4865Allow 'rewrite ... in' to assert the resulting type "rewrite f ==> t in x" means that after applying the rewrite f, the required type of x must be t. This is primarily for readability of proofs built by successive rewritings.Edwin Brady13 years ago c1a4eacFull TT reflection and reificationJan Bessai14 years ago 265d9a4Improve elaboration efficiency by cutting down on excessive backtrackingEdwin Brady14 years ago 04d6f00A small amount of proof automation, via tactic reflectionEdwin Brady14 years ago cc716d7Make 'Type' the type of types instead of Sets ...after mailing list discussionEdwin Brady14 years ago 5c9a88auppercase modulenamesraichoo14 years ago