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
*
Fix function applications without labels (OCaml warning 6)
glondu
2010-09-28
*
Checker: remove some dead code
letouzey
2010-09-24
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Fix inconsistency in Prop/Set conversion check
glondu
2010-09-23
*
Explicit Mod_checking signature
glondu
2010-09-16
*
Sharing is not anymore broken by traverse_module.
soubiran
2010-09-15
*
Fix likely semantic typos
glondu
2010-09-15
*
Fix unescaped end-of-lines (OCaml warning 29)
glondu
2010-09-13
*
* checker/Safe_typing.LightenLibrary:
regisgia
2010-08-27
*
* (checker|kernel)/Safe_typing:
regisgia
2010-08-27
*
* (checker|kernel)/Safe_typing:
regisgia
2010-08-27
*
* checker/SafeTyping kernel/SafeTyping:
regisgia
2010-08-27
*
* lib/Flags: Replace dont_load_proofs by load_proofs since not loading
regisgia
2010-08-27
*
* Improve documentation of LightenLibrary.
regisgia
2010-08-27
*
* (checker|kernel)/Safe_typing: New LightenLibrary.
regisgia
2010-08-27
*
adpated the checker to handle coomutative cuts and lazyness
barras
2010-07-30
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
ported bug fix r13290 to checker
barras
2010-07-22
*
Fix typos
glondu
2010-06-02
*
Cleanup: remove code specific for ocaml 3.06
letouzey
2010-06-01
*
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-05-19
*
After the approval of Bruno, here the patch for the checker.
soubiran
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
kills a warning about vo in checker/safe_typing
letouzey
2010-03-18
*
fixed confusion between number of cstr arguments and number of pattern variab...
barras
2010-03-12
*
added validation of delta_resolver (which seem to have an impact on typing)
barras
2010-02-19
*
[checker] fixed vo validation problems, module incompatibilities remain
barras
2010-02-19
*
* Segmenttree: New. A very simple implementation of segment trees.
regisgia
2010-01-08
*
* Rewrite [classify_unicode] using standard unicode tables.
regisgia
2009-12-20
*
fix coqchk options documentation
barras
2009-12-01
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Fix a small oversight in checker commit 12288.
herbelin
2009-08-23
*
Transfers to checker ("let"s in inductive arities + Coq root read-only).
herbelin
2009-08-22
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
Many changes in the Makefile infrastructure + a beginning of ocamlbuild
letouzey
2009-03-20
*
Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...
letouzey
2009-03-20
*
porting r11900 11905 and 11953 to trunk
barras
2009-03-02
*
Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk
notin
2009-02-11
*
Backporting from v8.2 to trunk:
herbelin
2009-01-18
*
Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...
notin
2009-01-06
*
Nettoyage des variables Coq et amélioration de coqmktop. Les
notin
2008-12-19
*
Report des commits 11417 et 11437 de la v8.2
soubiran
2008-10-15
*
fixed bug #1927 + univ constraints (module cstrs include cstrs of its subcomp...
barras
2008-09-02
*
[checker] basic conversion oracle: expand local vars first
barras
2008-09-02
*
fixed loop in dependency fold of the checker
barras
2008-07-24
*
Lissage de la gestion des chemins de chargement de fichiers :
herbelin
2008-06-29
*
doc of coqchk + improved module cache and computation of module sets
barras
2008-05-23
*
fixed dependency problems with the checker
barras
2008-05-22
*
added coqchk to the main Makefile and a make variable VALIDATE to check the v...
barras
2008-05-22
[next]