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
*
Make votour a bit more robust/forgiving with respect to user commands (bug #4...
Guillaume Melquiond
2016-05-02
*
Fix missing newline in coqchk engagement (bug #4694).
Guillaume Melquiond
2016-04-28
*
A patch renaming equal into eq in the module dealing with
Hugo Herbelin
2016-03-22
*
Rename Ephemeron -> CEphemeron.
Maxime Dénès
2016-03-04
*
Update cic.mli MD5 after header update.
Maxime Dénès
2016-01-20
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
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
*
Checker was forgetting to register global universes introduced by opaque
Matthieu Sozeau
2015-11-04
*
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
*
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
*
Univs/Inductive: fix typechecking of cases
Matthieu Sozeau
2015-07-15
*
Updating checksum in checker (9c732a5cc continued).
Hugo Herbelin
2015-07-12
*
Unused variables reported by OCaml.
Hugo Herbelin
2015-07-10
*
Option -type-in-type: added support in checker and making it contaminating
Hugo Herbelin
2015-07-10
*
Kernel/Checker: Cleanup fixes of substitutions due to let-ins.
Matthieu Sozeau
2015-07-09
*
Template polymorphism: A bug-fix for Bug #4258
mlasson
2015-07-09
*
Checker: Report bugfixes from kernel/inductive.ml
Matthieu Sozeau
2015-07-08
*
Checker: Fix bug #4282
Matthieu Sozeau
2015-07-07
*
Adding a more efficient representation of OCaml objects in votour.
Pierre-Marie Pédrot
2015-06-25
*
Moved fatal_error from Coqtop to Errors and corrected dependencies accordingly.
Thomas Sibut-Pinote
2015-06-25
*
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
*
Votour displays wordsize of segments before loading them.
Pierre-Marie Pédrot
2015-06-20
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Removing references to deprecated syntax -I/-R -as.
Pierre-Marie Pédrot
2015-03-31
*
Exporting memory representation of STM tasks for votour.
Pierre-Marie Pédrot
2015-03-25
*
Functorized interface over object representation in votour.
Pierre-Marie Pédrot
2015-03-24
*
Fixing representation of dynamics in votour (again).
Pierre-Marie Pédrot
2015-03-24
*
coqchk: more prints when -debug
Enrico Tassi
2015-03-23
*
Fixing internal representation of Dyn.t in votour.
Pierre-Marie Pédrot
2015-03-18
*
Now accepting unit props in mutual definitions
Bruno Barras
2015-03-02
*
Fix checker after addition of a universe context in with t := c constraints.
Matthieu Sozeau
2015-02-26
*
Revert "Using same code for browsing physical directories in coqtop and coqdep."
Hugo Herbelin
2015-02-12
*
Revert "Capital letter in plugins." (Sorry, was not intended to be pushed)
Hugo Herbelin
2015-02-12
*
Capital letter in plugins.
Hugo Herbelin
2015-02-12
*
Using same code for browsing physical directories in coqtop and coqdep.
Hugo Herbelin
2015-02-12
*
Fixing bug #4019, and checker blow-up at once.
Pierre-Marie Pédrot
2015-02-11
*
Clarifying the implementation of universe hashconsing.
Pierre-Marie Pédrot
2015-02-11
*
Windows: open .vo files in binary mode
Enrico Tassi
2015-02-05
*
Update hash of cic.mli in checker/values.ml,
Matthieu Sozeau
2015-01-13
*
Update headers.
Maxime Dénès
2015-01-12
*
Declarations.mli refactoring: module_type_body = module_body
Pierre Letouzey
2015-01-11
*
Fix checker's treatment of template polymorphic
Matthieu Sozeau
2015-01-06
*
rename: vi -> vio
Enrico Tassi
2015-01-06
*
updated include file for debugging
Bruno Barras
2015-01-06
[next]