aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/heads.ml
Commit message (Expand)AuthorAge
* Getting rid of the const_proj field in the kernel.Gravatar Pierre-Marie Pédrot2018-06-17
* Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Safer API for Global.body_of_constant and variants.Gravatar Pierre-Marie Pédrot2017-07-13
* Moving the last bits of abtraction-breaking code out of the kernel.Gravatar Pierre-Marie Pédrot2017-07-11
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Use Names.Constant.printGravatar Jason Gross2017-06-02
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Update headers.Gravatar Maxime Dénès2015-01-12
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Add a boolean to indicate the unfolding state of a primitive projection,Gravatar Matthieu Sozeau2014-09-27
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* heads: avoid forcing opaque proofsGravatar Enrico Tassi2014-05-15
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Fixing a Pervasive.compare.Gravatar Pierre-Marie Pédrot2014-02-28
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Minor code cleaning in CArray / CList.Gravatar ppedrot2013-03-23
* Fixed bug #2966 (de Bruijn error in computation of heads for coercions).Gravatar herbelin2013-01-28
* Monomorphization (library)Gravatar ppedrot2012-11-22
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* Heads: avoid potentially uncaught Not_found via an assert falseGravatar letouzey2011-10-24
* Temporary revert commit 14550 since it breaks a few contribsGravatar letouzey2011-10-12
* in heads.ml, at least turn the Not_found of #2608 into assert falseGravatar letouzey2011-10-11
* Heads: generic equality on constr replaced by destructorGravatar puech2011-07-29
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Some dead code removal + cleanupsGravatar letouzey2009-04-08
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
* Ajout propriété svn:keywords aux nouveaux fichiers du commit 10840Gravatar herbelin2008-04-24
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-27 06:01:22 +0000