index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
checker
/
check.ml
Commit message (
Expand
)
Author
Age
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
*
[cleanup] Unify all calls to the error function.
Emilio Jesus Gallego Arias
2017-05-27
*
Merge branch 'v8.6'
Pierre-Marie Pédrot
2016-10-02
|
\
*
|
Make the user_err header an optional parameter.
Emilio Jesus Gallego Arias
2016-08-19
*
|
Remove errorlabstrm in favor of user_err
Emilio Jesus Gallego Arias
2016-08-19
|
*
[checker] Fix/fine tune printing.
Emilio Jesus Gallego Arias
2016-08-18
|
/
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-09
|
\
|
*
Fix incorrect checking of library checksums.
Maxime Dénès
2016-06-05
*
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
/
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
Checker was forgetting to register global universes introduced by opaque
Matthieu Sozeau
2015-11-04
*
Make the interface of System.raw_extern_intern much saner.
Guillaume Melquiond
2015-09-29
*
On-demand Require.
Pierre-Marie Pédrot
2015-06-24
*
Splitting the library representation on disk in two.
Pierre-Marie Pédrot
2015-06-24
*
Windows: open .vo files in binary mode
Enrico Tassi
2015-02-05
*
Update headers.
Maxime Dénès
2015-01-12
*
rename: vi -> vio
Enrico Tassi
2015-01-06
*
Fix sigsegv in checker
Enrico Tassi
2014-12-19
*
vi2vo: universes handling finally fixed
Enrico Tassi
2014-03-11
*
checker and votour ported to new vo format (after -vi2vo)
Enrico Tassi
2014-02-26
*
.vi files: .vo files without proofs
Enrico Tassi
2014-01-04
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
Change in vo format : digest aren't Marshalled anymore
letouzey
2013-08-22
*
Uniformizing the [if_warn] flag used for warning printing and put
ppedrot
2013-05-08
*
Checker: vo validation is now done in check.ml (and always)
letouzey
2013-04-15
*
Checker: reified encoding of .vo types in values.ml
letouzey
2013-04-15
*
Checker: regroup all vo-related types in cic.mli
letouzey
2013-04-15
*
Revised infrastructure for lazy loading of opaque proofs
letouzey
2013-04-02
*
Safe_typing+Libary: use some arrays instead of lists in vo structures
letouzey
2013-03-28
*
Removing mandatory suffixes for library files.
ppedrot
2013-03-21
*
Restrict (try...with...) to avoid catching critical exn (part 1)
letouzey
2013-03-12
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Minor code cleanups, especially take advantage of Dir_path.is_empty
letouzey
2013-02-18
*
Fixing coqchk compilation after commit r16183
ppedrot
2013-02-03
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of dir_path
ppedrot
2012-12-14
*
Modulification of identifier
ppedrot
2012-12-14
*
Cleaning and small optimization in CList.
ppedrot
2012-11-20
*
Cleaning interface of Util.
ppedrot
2012-09-18
*
Moving Utils.list_* to a proper CList module, which includes stdlib
ppedrot
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Getting rid of Pp.msgnl and Pp.message.
ppedrot
2012-06-01
*
Getting rid of Pp.msg
ppedrot
2012-05-30
*
lib directory is cut in 2 cma.
pboutill
2012-04-12
*
Noise for nothing
pboutill
2012-03-02
*
Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks
letouzey
2011-04-03
*
Fix function applications without labels (OCaml warning 6)
glondu
2010-09-28
*
Checker: remove some dead code
letouzey
2010-09-24
[next]