aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* STM: proof state also includes meta countersGravatar Enrico Tassi2015-02-25
* Refactoring in [Constr].Gravatar Arnaud Spiwack2015-02-24
* Fix some typos in comments.Gravatar Guillaume Melquiond2015-02-23
* Fixing 934761875 about optimizing Import of several libraries at once (thanks...Gravatar Hugo Herbelin2015-02-23
* Documenting the caveat of assumption printing in the mli.Gravatar Pierre-Marie Pédrot2015-02-21
* Tentative fix for bug #4078.Gravatar Pierre-Marie Pédrot2015-02-21
* More resilient implementation of Print Assumptions.Gravatar Pierre-Marie Pédrot2015-02-21
* Deprecated options issue a warning.Gravatar Pierre-Marie Pédrot2015-02-17
* Fixing bug #4053.Gravatar Pierre-Marie Pédrot2015-02-17
* Better comment for [type_of_global_unsafe].Gravatar Matthieu Sozeau2015-02-16
* Comment on the unsafe_ functions in Global.Gravatar Matthieu Sozeau2015-02-16
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* Windows: open .vo files in binary modeGravatar Enrico Tassi2015-02-05
* Properly set module names in presence of -Q. (Fix for bug #3958)Gravatar Guillaume Melquiond2015-02-05
* Optimized Import/Export the same way as Require Import/Export wasGravatar Hugo Herbelin2015-02-04
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Remove dead code.Gravatar Maxime Dénès2015-01-17
* Univs: proper printing of global and local universe names (onlyGravatar Matthieu Sozeau2015-01-17
* Partially revert "Forbid Require inside interactive modules and module types."Gravatar Maxime Dénès2015-01-17
* Avoid compilation warning... might not be the best fix though.Gravatar Matthieu Sozeau2015-01-17
* Made -print-mod-uid more silent and robust.Gravatar Maxime Dénès2015-01-13
* Fix bug when discharging universe constraints coming from variablesGravatar Matthieu Sozeau2015-01-13
* fixup to vi -> vio renamingGravatar Enrico Tassi2015-01-12
* Update headers.Gravatar Maxime Dénès2015-01-12
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* kernel/ind Change interface of declare_mind and declare_mutualGravatar Matthieu Sozeau2015-01-05
* Forbid Require inside interactive modules and module types.Gravatar Maxime Dénès2014-12-25
* Summary: more surgery functionsGravatar Enrico Tassi2014-12-17
* Global: export the name of the summary entryGravatar Enrico Tassi2014-12-17
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Fix for #3154: use CUnix.sys_command to call native compiler.Gravatar Maxime Dénès2014-12-16
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Reverting the following block of three commits:Gravatar Hugo Herbelin2014-11-27
* Registering strict implicit arguments systematically.Gravatar Hugo Herbelin2014-11-26
* Pass around information on the use of template polymorphism forGravatar Matthieu Sozeau2014-11-23
* Universes.nf_evars_and_universes_opt_subst substitutes evars eagerly.Gravatar Pierre-Marie Pédrot2014-11-10
* Better error messages when unfreezing summary entriesGravatar Enrico Tassi2014-10-30
* When loading libraries, feed back dependencies.Gravatar Carst Tankink2014-10-13
* STM: primitives to snapshot a .vi while in interactive modeGravatar Enrico Tassi2014-10-13
* selective join/export of the safe_environmentGravatar Enrico Tassi2014-10-13
* STM: simplify how the term part of a side effect is retrievedGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* Index keys instead of simply global references.Gravatar Matthieu Sozeau2014-09-27
* First version of keyed subterm selection in unification.Gravatar Matthieu Sozeau2014-09-27
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Make eq_pattern_test/eq_test work up to the equivalence of primitiveGravatar Matthieu Sozeau2014-09-24
* Providing a -type-in-type option for collapsing the universe hierarchy.Gravatar Hugo Herbelin2014-09-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 12:03:25 +0000