aboutsummaryrefslogtreecommitdiff
path: root/library/library.mllib
AgeCommit message (Expand)Author
2019-09-18[library] Move `Declaremods` to `vernac/`Emilio Jesus Gallego Arias
2019-08-30[library] Move library to vernacEmilio Jesus Gallego Arias
2019-08-23Merge PR #10665: [api] Move handling of variable implicit data to impargsGaëtan Gilbert
2019-08-19[api] Move handling of variable implicit data to impargsEmilio Jesus Gallego Arias
2019-08-18[api] Move `Keys` to pretypingEmilio Jesus Gallego Arias
2019-07-01[api] Refactor most of `Decl_kinds`Emilio Jesus Gallego Arias
2019-05-21[loadpath] Make loadpath handling self-contained and move to vernacEmilio Jesus Gallego Arias
2018-09-18Removing Dischargedhypsmap which is unused internally.Maxime Dénès
2018-07-24Move Heads to pretyping (is_projection will move to Recordops)Gaëtan Gilbert
2018-06-12[api] Remove Misctypes.Emilio Jesus Gallego Arias
2018-04-23[api] Relocate `intf` modules according to dependency-order.Emilio Jesus Gallego Arias
2017-11-21[api] Miscellaneous consolidation + moves to engine.Emilio Jesus Gallego Arias
2017-06-16Move univops from kernel to libraryAmin Timany
2017-05-27[coqlib] Move `Coqlib` to `library/`.Emilio Jesus Gallego Arias
2016-10-30Moving Universes to the engine/ folder.Pierre-Marie Pédrot
2015-06-29Assumptions: more informative print for False axiom (Close: #4054)Enrico Tassi
2014-09-27Index keys instead of simply global references.Matthieu Sozeau
2014-09-27First version of keyed subterm selection in unification.Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-03-26Moved the Loadpath part of Library to its own file, and documentedppedrot
2012-08-24correct some ends of .mllib files (avoid a broken tolink.ml)letouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlletouzey
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ...letouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-03-20Many changes in the Makefile infrastructure + a beginning of ocamlbuildletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:46:48 +0000