index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
plugins
/
cc
/
ccproof.ml
Commit message (
Expand
)
Author
Age
*
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
*
Fixing a source of inefficiency and an artificial dependency in the
Daniel de Rauglaudre
2016-04-08
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Update headers.
Maxime Dénès
2015-01-12
*
fix bug #2447 in congruence
Pierre Corbineau
2014-12-16
*
Revert "Fixing a loop in proof reconstruction for congruence (#2447)."
Hugo Herbelin
2014-10-17
*
Fixing a loop in proof reconstruction for congruence (#2447).
Hugo Herbelin
2014-10-17
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
Partial revert of Yann commit in order to use CLib.List when opening
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Noise for nothing
pboutill
2012-03-02
*
Ccalgo, Ccproof: multiple generic Hashtbl on constr and term replaced by Cons...
puech
2011-07-29
*
Ccproof: generic equality on term replaced by term_equal
puech
2011-07-29
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2009-03-20