aboutsummaryrefslogtreecommitdiff
path: root/library/heads.ml
AgeCommit message (Expand)Author
2018-07-24Move Heads to pretyping (is_projection will move to Recordops)Gaëtan Gilbert
2018-06-17Getting rid of the const_proj field in the kernel.Pierre-Marie Pédrot
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-07-13Safer API for Global.body_of_constant and variants.Pierre-Marie Pédrot
2017-07-11Moving the last bits of abtraction-breaking code out of the kernel.Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-02Use Names.Constant.printJason Gross
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-02-09CLEANUP: Context.{Rel,Named}.Declaration.tMatej Kosik
2016-01-20Update copyright headers.Maxime Dénès
2015-10-28Avoid type checking private_constants (side_eff) again during Qed (#4357).Enrico Tassi
2015-01-12Update headers.Maxime Dénès
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-09-27Add a boolean to indicate the unfolding state of a primitive projection,Matthieu Sozeau
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-05-15heads: avoid forcing opaque proofsEnrico Tassi
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-02-28Fixing a Pervasive.compare.Pierre-Marie Pédrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-22code simplifications concerning Summaryletouzey
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-01-28Fixed bug #2966 (de Bruijn error in computation of heads for coercions).herbelin
2012-11-22Monomorphization (library)ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-02Noise for nothingpboutill
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-10-24Heads: avoid potentially uncaught Not_found via an assert falseletouzey
2011-10-12Temporary revert commit 14550 since it breaks a few contribsletouzey
2011-10-11in heads.ml, at least turn the Not_found of #2608 into assert falseletouzey
2011-07-29Heads: generic equality on constr replaced by destructorpuech
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Remove useless Liboject.export_function fieldglondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-04-08Some dead code removal + cleanupsletouzey
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
2008-04-24Ajout propriété svn:keywords aux nouveaux fichiers du commit 10840herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 22:51:28 +0000