index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
/
heads.ml
Commit message (
Expand
)
Author
Age
*
Safer API for Global.body_of_constant and variants.
Pierre-Marie Pédrot
2017-07-13
*
Moving the last bits of abtraction-breaking code out of the kernel.
Pierre-Marie Pédrot
2017-07-11
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Use Names.Constant.print
Jason Gross
2017-06-02
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Avoid type checking private_constants (side_eff) again during Qed (#4357).
Enrico Tassi
2015-10-28
*
Update headers.
Maxime Dénès
2015-01-12
*
library/opaqueTables: enable their use in interactive mode
Enrico Tassi
2014-10-13
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
heads: avoid forcing opaque proofs
Enrico Tassi
2014-05-15
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Fixing a Pervasive.compare.
Pierre-Marie Pédrot
2014-02-28
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
code simplifications concerning Summary
letouzey
2013-04-22
*
Minor code cleaning in CArray / CList.
ppedrot
2013-03-23
*
Fixed bug #2966 (de Bruijn error in computation of heads for coercions).
herbelin
2013-01-28
*
Monomorphization (library)
ppedrot
2012-11-22
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Add type annotations around all calls to Libobject.declare_object
letouzey
2011-11-02
*
Heads: avoid potentially uncaught Not_found via an assert false
letouzey
2011-10-24
*
Temporary revert commit 14550 since it breaks a few contribs
letouzey
2011-10-12
*
in heads.ml, at least turn the Not_found of #2608 into assert false
letouzey
2011-10-11
*
Heads: generic equality on constr replaced by destructor
puech
2011-07-29
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Remove useless Liboject.export_function field
glondu
2009-09-17
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Death of "survive_module" and "survive_section" (the first one was
herbelin
2009-08-13
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
Correct implementation of discharging of implicit arguments and add new
msozeau
2008-07-22
*
Ajout propriété svn:keywords aux nouveaux fichiers du commit 10840
herbelin
2008-04-24
*
Prise en compte des coercions dans les clauses "with" même si le type
herbelin
2008-04-23