aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2015-02-23Fixing 934761875 about optimizing Import of several libraries at once (thanks...Hugo Herbelin
2015-02-21Documenting the caveat of assumption printing in the mli.Pierre-Marie Pédrot
2015-02-21Tentative fix for bug #4078.Pierre-Marie Pédrot
2015-02-21More resilient implementation of Print Assumptions.Pierre-Marie Pédrot
2015-02-17Deprecated options issue a warning.Pierre-Marie Pédrot
2015-02-17Fixing bug #4053.Pierre-Marie Pédrot
2015-02-16Better comment for [type_of_global_unsafe].Matthieu Sozeau
2015-02-16Comment on the unsafe_ functions in Global.Matthieu Sozeau
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
2015-02-05Windows: open .vo files in binary modeEnrico Tassi
2015-02-05Properly set module names in presence of -Q. (Fix for bug #3958)Guillaume Melquiond
2015-02-04Optimized Import/Export the same way as Require Import/Export wasHugo Herbelin
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-17Remove dead code.Maxime Dénès
2015-01-17Univs: proper printing of global and local universe names (onlyMatthieu Sozeau
2015-01-17Partially revert "Forbid Require inside interactive modules and module types."Maxime Dénès
2015-01-17Avoid compilation warning... might not be the best fix though.Matthieu Sozeau
2015-01-13Made -print-mod-uid more silent and robust.Maxime Dénès
2015-01-13Fix bug when discharging universe constraints coming from variablesMatthieu Sozeau
2015-01-12fixup to vi -> vio renamingEnrico Tassi
2015-01-12Update headers.Maxime Dénès
2015-01-11Declarations.mli refactoring: module_type_body = module_bodyPierre Letouzey
2015-01-05kernel/ind Change interface of declare_mind and declare_mutualMatthieu Sozeau
2014-12-25Forbid Require inside interactive modules and module types.Maxime Dénès
2014-12-17Summary: more surgery functionsEnrico Tassi
2014-12-17Global: export the name of the summary entryEnrico Tassi
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-16Fix for #3154: use CUnix.sys_command to call native compiler.Maxime Dénès
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-11-27Reverting the following block of three commits:Hugo Herbelin
2014-11-26Registering strict implicit arguments systematically.Hugo Herbelin
2014-11-23Pass around information on the use of template polymorphism forMatthieu Sozeau
2014-11-10Universes.nf_evars_and_universes_opt_subst substitutes evars eagerly.Pierre-Marie Pédrot
2014-10-30Better error messages when unfreezing summary entriesEnrico Tassi
2014-10-13When loading libraries, feed back dependencies.Carst Tankink
2014-10-13STM: primitives to snapshot a .vi while in interactive modeEnrico Tassi
2014-10-13selective join/export of the safe_environmentEnrico Tassi
2014-10-13STM: simplify how the term part of a side effect is retrievedEnrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-09-27Index keys instead of simply global references.Matthieu Sozeau
2014-09-27First version of keyed subterm selection in unification.Matthieu Sozeau
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-09-24Make eq_pattern_test/eq_test work up to the equivalence of primitiveMatthieu Sozeau
2014-09-13Providing a -type-in-type option for collapsing the universe hierarchy.Hugo Herbelin
2014-09-10Parsing and printing of primitive projections, fix buggy behavior whenMatthieu Sozeau
2014-09-09- Fix printing and parsing of primitive projections, including the SetMatthieu Sozeau
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-09-04Print [Variant] types with the keyword [Variant].Arnaud Spiwack
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 11:46:11 +0000