aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-06-15- Fix xml plugin treatment of inductives.Matthieu Sozeau
2014-06-13Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead of...Matthieu Sozeau
2014-06-13HoTT/coq bug #7 is closed, and the definitions can be made to go through usin...Matthieu Sozeau
2014-06-13Deprecate useless option -quality.Guillaume Melquiond
2014-06-13Remove documentation for the unsupported options -byte and -opt.Guillaume Melquiond
2014-06-13Deprecate useless option -unsafe.Guillaume Melquiond
2014-06-13Deprecate options -dont, -lazy, -force-load-proofs.Guillaume Melquiond
2014-06-13Less ocaml warnings.Hugo Herbelin
2014-06-13Improving tclWITHHOLES which did not see undefined evars up toHugo Herbelin
2014-06-13Fixing "clear" in internal_cut_replace: forbid dependencies in theHugo Herbelin
2014-06-13Improved error message when a meta posed as an evar remains unsolvedHugo Herbelin
2014-06-13Check resolution of Metas turned into Evars by pose_all_metas_as_evarsHugo Herbelin
2014-06-13Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).Hugo Herbelin
2014-06-13Adapt simpl/cbn unfolding and refolding machinery to projections, so thatMatthieu Sozeau
2014-06-12Code cleaning in Univ.Pierre-Marie Pédrot
2014-06-12Passing some tactics to the new monad type.Pierre-Marie Pédrot
2014-06-11Fix bug #3291, stack overflow in rewrite.Matthieu Sozeau
2014-06-11Fix bug #3289Matthieu Sozeau
2014-06-11Move bug # 3368 to closed bugsMatthieu Sozeau
2014-06-11Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into trunkMatthieu Sozeau
2014-06-11- Fix bug #3368, due to wrong use of the Cst_stack for projections.Matthieu Sozeau
2014-06-11In generalized rewrite, avoid retyping completely and constantly the conclusi...Matthieu Sozeau
2014-06-11fix handling of side effects in abstract (fixes QArithSternBrocot)Enrico Tassi
2014-06-10Add many more cases to the test-suiteJason Gross
2014-06-10Move closed bug 3314Jason Gross
2014-06-10Add a test-case for bug #3314 proving FalseJason Gross
2014-06-10Fixing Sorting Universes in a world where le and lt constraints may bePierre-Marie Pédrot
2014-06-10Compute the trace of a universe inconsistency only when explicitly requiredPierre-Marie Pédrot
2014-06-10Made explanations for universe inconsistencies optional. They are only usedPierre-Marie Pédrot
2014-06-10Specialize the type of [Univ.compare_neq] so that it is clear it is only usedPierre-Marie Pédrot
2014-06-10Removing dead code in checker/univ.ml.Pierre-Marie Pédrot
2014-06-10Removing explanations of universe inconsistencies from the checker. TheyPierre-Marie Pédrot
2014-06-10Imperatively check touched universes in compare_neq functions. This ensuresPierre-Marie Pédrot
2014-06-10Providing the checker with its own version of the Univ file.Pierre-Marie Pédrot
2014-06-10- Fix substitution of universes which needlessly hashconsed existing universes.Matthieu Sozeau
2014-06-10Oops, one refactoring was not compiled.Matthieu Sozeau
2014-06-10More cleanup/reorganizing of univ.ml to separate constraint/universe handling...Matthieu Sozeau
2014-06-10Fix module order in printers.mllibMatthieu Sozeau
2014-06-10Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...Matthieu Sozeau
2014-06-10Remove unused function in univMatthieu Sozeau
2014-06-10Merge branch 'hott-test-suite-progress' of https://github.com/JasonGross/coq ...Matthieu Sozeau
2014-06-09Flattening Level module structure in Univ.Pierre-Marie Pédrot
2014-06-08Mark some progress in the HoTT/coq test-suiteJason Gross
2014-06-08Adding a toplevel option allowing to deactivate the term sharing in kernelPierre-Marie Pédrot
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-06-08Fix canonical structure resolution in unification (bug found in Ssreflect).Matthieu Sozeau
2014-06-08Timeout implementation for Windows based on threads.Pierre-Marie Pédrot
2014-06-08Enforce a correct exception handling in declaration_hooksEnrico Tassi
2014-06-08ind_tables: always declare side effects (Closes: HOTT#110)Enrico Tassi
2014-06-08STM: handle "Time Abort" correctly (Closes: 3332)Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 02:24:48 +0000