index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
checker
Commit message (
Expand
)
Author
Age
*
Merge PR #244.
Pierre-Marie Pédrot
2016-09-08
|
\
|
*
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
|
*
Unify location handling of error functions.
Emilio Jesus Gallego Arias
2016-08-19
|
/
*
remove checker/Makefile
Pierre Letouzey
2016-07-26
*
Merge remote-tracking branch 'gforge/v8.5' into v8.6
Matthieu Sozeau
2016-07-26
|
\
|
*
Fix bug #4876: critical bug in guard condition checker.
Matthieu Sozeau
2016-07-25
*
|
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
|
Separate flags for fix/cofix/match reduction and clean reduction function names.
Maxime Dénès
2016-07-01
*
|
A new infrastructure for warnings.
Maxime Dénès
2016-06-29
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-27
|
\
|
|
*
Remove extraction-specific code from the checker.
Guillaume Melquiond
2016-06-23
*
|
Fixing the checker.
Pierre-Marie Pédrot
2016-06-18
*
|
Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.
Pierre-Marie Pédrot
2016-06-16
|
\
\
|
*
|
Fixing the checker.
Pierre-Marie Pédrot
2016-06-16
*
|
|
Preventive compatibility fixes for flushing.
Emilio Jesus Gallego Arias
2016-06-14
*
|
|
configure: use ln on linux and cp on windows
Enrico Tassi
2016-06-14
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-06-09
|
\
\
\
|
|
|
/
|
|
/
|
|
*
|
Do not use COQLIBS for the validate rule produced by coq_makefile (bug #4693).
Guillaume Melquiond
2016-06-07
|
*
|
Fix incorrect checking of library checksums.
Maxime Dénès
2016-06-05
*
|
|
Merge branch 'yet-another-makefile-bigbang' into trunk
Pierre Letouzey
2016-06-01
|
\
\
\
|
*
|
|
Makefile: restore the use of coqdep_boot for creating .v.d files
Pierre Letouzey
2016-06-01
*
|
|
|
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
|
/
/
/
*
|
|
Checker: avoid using obsolete names from Names
Pierre Letouzey
2016-05-31
*
|
|
Checker: no more -I kernel via a few symlinks (for Names and Esubst)
Pierre Letouzey
2016-05-31
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-04
|
\
|
|
|
*
|
Make votour a bit more robust/forgiving with respect to user commands (bug #4...
Guillaume Melquiond
2016-05-02
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-05-02
|
\
|
|
|
*
|
Fix missing newline in coqchk engagement (bug #4694).
Guillaume Melquiond
2016-04-28
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-30
|
\
|
|
|
*
|
A patch renaming equal into eq in the module dealing with
Hugo Herbelin
2016-03-22
*
|
|
Removing OCaml deprecated function names from the Lazy module.
Pierre-Marie Pédrot
2016-03-10
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-03-05
|
\
|
|
|
*
|
Rename Ephemeron -> CEphemeron.
Maxime Dénès
2016-03-04
*
|
|
CLEANUP: Simplifying the changes done in "checker/*"
Matej Kosik
2016-02-15
*
|
|
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
|
|
*
|
Update cic.mli MD5 after header update.
Maxime Dénès
2016-01-20
|
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
|
Remove deprecated command-line options such as "-as".
Guillaume Melquiond
2016-01-06
*
|
|
Merge remote-tracking branch 'origin/v8.5' into trunk
Guillaume Melquiond
2016-01-06
|
\
|
|
|
*
|
Protect code against changes in Map interface.
Maxime Dénès
2016-01-06
|
*
|
Fix order of files in mllib.
Maxime Dénès
2016-01-05
*
|
|
Remove unused function Checker.print_loc.
Guillaume Melquiond
2015-12-31
*
|
|
Do not compose "str" and "to_string" whenever possible.
Guillaume Melquiond
2015-12-22
*
|
|
Factorizing unsafe code by relying on the new Dyn module.
Pierre-Marie Pédrot
2015-12-05
*
|
|
Displaying the object identifier in votour.
Pierre-Marie Pédrot
2015-11-15
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-05
|
\
|
|
|
*
|
Checker was forgetting to register global universes introduced by opaque
Matthieu Sozeau
2015-11-04
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
|
|
[next]