aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Fix type inference of the record argument of a projection to catch ill-typedGravatar Matthieu Sozeau2014-06-17
* - Fix the de Bruijn problem in check_projection for good :)Gravatar Matthieu Sozeau2014-06-17
* Fix a de Bruijn bug in checking code of projections.Gravatar Matthieu Sozeau2014-06-17
* Safer entry point of primitive projections in the kernel, now it does recognizeGravatar Matthieu Sozeau2014-06-17
* Existing Class now works with universe polymorphism. Fixes HoTT bug #063Gravatar Matthieu Sozeau2014-06-17
* Improve hotspot in Auto.Gravatar Pierre-Marie Pédrot2014-06-17
* Checking that a library name is valid before compilation.Gravatar Pierre-Marie Pédrot2014-06-16
* Unification in HoTT_coq_061.v was looping with previous commit (whileGravatar Hugo Herbelin2014-06-16
* Fixing part of HoTT bug #61 (in declare_evar_from_virtual_equation,Gravatar Hugo Herbelin2014-06-16
* - Add "Show Universes" to print information about universes during a proof.Gravatar Matthieu Sozeau2014-06-16
* HoTT bug #29 is fixed, using the correct notion of polymorphic product types.Gravatar Matthieu Sozeau2014-06-16
* Fix spacing in error message.Gravatar Guillaume Melquiond2014-06-16
* Preemptively remove files from native compilation.Gravatar Guillaume Melquiond2014-06-16
* Fix test-suite fileGravatar Matthieu Sozeau2014-06-15
* Change Ltac constr matching semantics to consider universes when merging twoGravatar Matthieu Sozeau2014-06-15
* The semantics of Variable x y : T is to have the exact same type T for x and y,Gravatar Matthieu Sozeau2014-06-15
* Remove HoTT bug #33, as the stdlib won't become polymorphic in the next version.Gravatar Matthieu Sozeau2014-06-15
* - Fix xml plugin treatment of inductives.Gravatar Matthieu Sozeau2014-06-15
* Fix HoTT/coq bug # 14. Now coercion code correctly raises an error instead of...Gravatar Matthieu Sozeau2014-06-13
* HoTT/coq bug #7 is closed, and the definitions can be made to go through usin...Gravatar Matthieu Sozeau2014-06-13
* Deprecate useless option -quality.Gravatar Guillaume Melquiond2014-06-13
* Remove documentation for the unsupported options -byte and -opt.Gravatar Guillaume Melquiond2014-06-13
* Deprecate useless option -unsafe.Gravatar Guillaume Melquiond2014-06-13
* Deprecate options -dont, -lazy, -force-load-proofs.Gravatar Guillaume Melquiond2014-06-13
* Less ocaml warnings.Gravatar Hugo Herbelin2014-06-13
* Improving tclWITHHOLES which did not see undefined evars up toGravatar Hugo Herbelin2014-06-13
* Fixing "clear" in internal_cut_replace: forbid dependencies in theGravatar Hugo Herbelin2014-06-13
* Improved error message when a meta posed as an evar remains unsolvedGravatar Hugo Herbelin2014-06-13
* Check resolution of Metas turned into Evars by pose_all_metas_as_evarsGravatar Hugo Herbelin2014-06-13
* Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).Gravatar Hugo Herbelin2014-06-13
* Adapt simpl/cbn unfolding and refolding machinery to projections, so thatGravatar Matthieu Sozeau2014-06-13
* Code cleaning in Univ.Gravatar Pierre-Marie Pédrot2014-06-12
* Passing some tactics to the new monad type.Gravatar Pierre-Marie Pédrot2014-06-12
* Fix bug #3291, stack overflow in rewrite.Gravatar Matthieu Sozeau2014-06-11
* Fix bug #3289Gravatar Matthieu Sozeau2014-06-11
* Move bug # 3368 to closed bugsGravatar Matthieu Sozeau2014-06-11
* Merge branch 'more-test-suite' of https://github.com/JasonGross/coq into trunkGravatar Matthieu Sozeau2014-06-11
|\
* | - Fix bug #3368, due to wrong use of the Cst_stack for projections.Gravatar Matthieu Sozeau2014-06-11
* | In generalized rewrite, avoid retyping completely and constantly the conclusi...Gravatar Matthieu Sozeau2014-06-11
* | fix handling of side effects in abstract (fixes QArithSternBrocot)Gravatar Enrico Tassi2014-06-11
| * Add many more cases to the test-suiteGravatar Jason Gross2014-06-10
| * Move closed bug 3314Gravatar Jason Gross2014-06-10
| * Add a test-case for bug #3314 proving FalseGravatar Jason Gross2014-06-10
|/
* Fixing Sorting Universes in a world where le and lt constraints may beGravatar Pierre-Marie Pédrot2014-06-10
* Compute the trace of a universe inconsistency only when explicitly requiredGravatar Pierre-Marie Pédrot2014-06-10
* Made explanations for universe inconsistencies optional. They are only usedGravatar Pierre-Marie Pédrot2014-06-10
* Specialize the type of [Univ.compare_neq] so that it is clear it is only usedGravatar Pierre-Marie Pédrot2014-06-10
* Removing dead code in checker/univ.ml.Gravatar Pierre-Marie Pédrot2014-06-10
* Removing explanations of universe inconsistencies from the checker. TheyGravatar Pierre-Marie Pédrot2014-06-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-08-16 15:27:39 +0000