aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-22Tactical `progress` compares term up to potentially equalisable universes.Arnaud Spiwack
2015-04-17Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of severalHugo Herbelin
2015-04-09Strengthen minimization: it shouldn't set a universe u to a max if itMatthieu Sozeau
2015-04-02Make it possible for -R to override the existing implicit setting of a path.Guillaume Melquiond
2015-04-01From X Require Y looks for X with absolute path, disregarding -R.Pierre-Marie Pédrot
2015-04-01Removing a probably incorrect on-the-fly require in a tactic.Pierre-Marie Pédrot
2015-03-31Removing the unused root flag from loadpaths.Pierre-Marie Pédrot
2015-03-31A more reasonable implementation of Loadpath.Pierre-Marie Pédrot
2015-03-25Summary: fix code to detect functional values in summaryEnrico Tassi
2015-03-23Dedicated type for on-demand objects in Library.Pierre-Marie Pédrot
2015-03-16Removing the whole library content from the summary.Pierre-Marie Pédrot
2015-03-16More invariants in Library.Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-02-25STM: proof state also includes meta countersEnrico Tassi
2015-02-24Refactoring in [Constr].Arnaud Spiwack
2015-02-23Fix some typos in comments.Guillaume Melquiond
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 15:11:28 +0000