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
*
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