aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2014-05-22Fix native_compute for systems with a limited size for the command line.Guillaume Melquiond
2014-05-16Declare: fix Future managementEnrico Tassi
2014-05-15heads: avoid forcing opaque proofsEnrico Tassi
2014-05-11Eliminating a potentially quadratic behaviour in Require, by using mapsPierre-Marie Pédrot
2014-05-06Fix extraction taking a type in the wrong environment.Matthieu Sozeau
2014-05-06Avoid u+k <= v constraints, don't take the sup of an algebraic universe duringMatthieu Sozeau
2014-05-06- Add back some compatibility functions to avoid rewriting plugins.Matthieu Sozeau
2014-05-06- Fix arity handling in retyping (de Bruijn bug!)Matthieu Sozeau
2014-05-06Fix restrict_universe_context removing some universes that do appear in the t...Matthieu Sozeau
2014-05-06Fix restrict_universe_context to not remove useful constraints.Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Matthieu Sozeau
2014-05-06Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Yves Bertot
2014-05-06- Fix abstract forgetting about new constraints.Matthieu Sozeau
2014-05-06- Fix handling of polymorphic inductive elimination schemes.Matthieu Sozeau
2014-05-06Fix printing of projections with implicits.Matthieu Sozeau
2014-05-06- Fix comparison of universes.Matthieu Sozeau
2014-05-06- Rename eq to equal in Univ, document new modules, set interfaces.Matthieu Sozeau
2014-05-06Fix interface for template polymorphism, cleaning up code in all typing algor...Matthieu Sozeau
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06Rework handling of universes on top of the STM, allowing for delayedMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-05-01Fixing ml-doc.Pierre-Marie Pédrot
2014-04-29Native compiler: hide compiled files in a .coq-native subdirectory.Maxime Dénès
2014-04-25Fixing various backtrace recordings.Pierre-Marie Pédrot
2014-04-23Removing dead code, thanks to new OCaml warnings and a bit of scripting.Pierre-Marie Pédrot
2014-04-08Add an option -Q (tentative name).Guillaume Melquiond
2014-04-02Fix Bug 3217Pierre Boutillier
2014-03-20Missing equalities in Names-like structures.Pierre-Marie Pédrot
2014-03-18STM: make -async-proofs on work from coqc tooEnrico Tassi
2014-03-14Changing Retrokwnoledge entry type from kind_of_term to constr. It seems it hadPierre-Marie Pédrot
2014-03-11vi2vo: universes handling finally fixedEnrico Tassi
2014-03-08Using HMaps in global references.Pierre-Marie Pédrot
2014-03-07Fix lookup of native files when option -R is missing.Guillaume Melquiond
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-03Goptions do not rely anymore on generic equality.Pierre-Marie Pédrot
2014-03-01Fixing pervasive comparisonsPierre-Marie Pédrot
2014-02-28Fixing a Pervasive.compare.Pierre-Marie Pédrot
2014-02-26Library: when compiling multiple files, reset the opaque tablesEnrico Tassi
2014-02-26Lazyconstr -> OpaqueproofEnrico Tassi
2014-02-26New compilation mode -vi2voEnrico Tassi
2014-02-03Allocation-friendly mapping functions in Nametab.Pierre-Marie Pédrot
2014-01-05STM: modules do not prevent proofs from being ASyncEnrico Tassi
2014-01-05coqtop: -check-vi-tasks and -schedule-vi-checkingEnrico Tassi
2014-01-04.vi files: .vo files without proofsEnrico Tassi
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-12-12Patch for supporting [From Xxx Require Yyy Zzz.]Gregory Malecha
2013-12-02Print logical name rather than path (thus allowing reproducible tests).xclerc
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 07:55:16 +0000