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 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
|
\
|
|
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-02
|
\
\
\
|
|
*
|
Univs: fix checker generating undeclared universes.
Matthieu Sozeau
2015-10-02
|
|
*
|
Univs: update checker
Matthieu Sozeau
2015-10-02
|
|
/
/
|
*
|
Make the interface of System.raw_extern_intern much saner.
Guillaume Melquiond
2015-09-29
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-09-06
|
\
|
|
|
*
|
Implementing Herbelin's fix for the "NonPar" bug
mlasson
2015-09-03
|
*
|
Reverting 16 last commits, committed mistakenly using the wrong push command.
Hugo Herbelin
2015-08-02
|
*
|
Hconsing continued
Hugo Herbelin
2015-08-02
*
|
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-07-18
|
\
|
|
|
*
|
Univs/Inductive: fix typechecking of cases
Matthieu Sozeau
2015-07-15
[next]