aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* - Fix hashing of levels to get the "right" order in universe contexts etc...Gravatar Matthieu Sozeau2014-06-04
* Fix native_compute for systems with a limited size for the command line.Gravatar Guillaume Melquiond2014-05-22
* Declare: fix Future managementGravatar Enrico Tassi2014-05-16
* heads: avoid forcing opaque proofsGravatar Enrico Tassi2014-05-15
* Eliminating a potentially quadratic behaviour in Require, by using mapsGravatar Pierre-Marie Pédrot2014-05-11
* Fix extraction taking a type in the wrong environment.Gravatar Matthieu Sozeau2014-05-06
* Avoid u+k <= v constraints, don't take the sup of an algebraic universe duringGravatar Matthieu Sozeau2014-05-06
* - Add back some compatibility functions to avoid rewriting plugins.Gravatar Matthieu Sozeau2014-05-06
* - Fix arity handling in retyping (de Bruijn bug!)Gravatar Matthieu Sozeau2014-05-06
* Fix restrict_universe_context removing some universes that do appear in the t...Gravatar Matthieu Sozeau2014-05-06
* Fix restrict_universe_context to not remove useful constraints.Gravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* - Fix abstract forgetting about new constraints.Gravatar Matthieu Sozeau2014-05-06
* - Fix handling of polymorphic inductive elimination schemes.Gravatar Matthieu Sozeau2014-05-06
* Fix printing of projections with implicits.Gravatar Matthieu Sozeau2014-05-06
* - Fix comparison of universes.Gravatar Matthieu Sozeau2014-05-06
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* Fix interface for template polymorphism, cleaning up code in all typing algor...Gravatar Matthieu Sozeau2014-05-06
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing ml-doc.Gravatar Pierre-Marie Pédrot2014-05-01
* Native compiler: hide compiled files in a .coq-native subdirectory.Gravatar Maxime Dénès2014-04-29
* Fixing various backtrace recordings.Gravatar Pierre-Marie Pédrot2014-04-25
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Add an option -Q (tentative name).Gravatar Guillaume Melquiond2014-04-08
* Fix Bug 3217Gravatar Pierre Boutillier2014-04-02
* Missing equalities in Names-like structures.Gravatar Pierre-Marie Pédrot2014-03-20
* STM: make -async-proofs on work from coqc tooGravatar Enrico Tassi2014-03-18
* Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadGravatar Pierre-Marie Pédrot2014-03-14
* vi2vo: universes handling finally fixedGravatar Enrico Tassi2014-03-11
* Using HMaps in global references.Gravatar Pierre-Marie Pédrot2014-03-08
* Fix lookup of native files when option -R is missing.Gravatar Guillaume Melquiond2014-03-07
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Goptions do not rely anymore on generic equality.Gravatar Pierre-Marie Pédrot2014-03-03
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* Fixing a Pervasive.compare.Gravatar Pierre-Marie Pédrot2014-02-28
* Library: when compiling multiple files, reset the opaque tablesGravatar Enrico Tassi2014-02-26
* Lazyconstr -> OpaqueproofGravatar Enrico Tassi2014-02-26
* New compilation mode -vi2voGravatar Enrico Tassi2014-02-26
* Allocation-friendly mapping functions in Nametab.Gravatar Pierre-Marie Pédrot2014-02-03
* STM: modules do not prevent proofs from being ASyncGravatar Enrico Tassi2014-01-05
* coqtop: -check-vi-tasks and -schedule-vi-checkingGravatar Enrico Tassi2014-01-05
* .vi files: .vo files without proofsGravatar Enrico Tassi2014-01-04
* Qed: feedback when type checking is doneGravatar Enrico Tassi2013-12-24
* Patch for supporting [From Xxx Require Yyy Zzz.]Gravatar Gregory Malecha2013-12-12
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 00:43:40 +0000