index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
checker
Age
Commit message (
Expand
)
Author
2010-06-02
Fix typos
glondu
2010-06-01
Cleanup: remove code specific for ocaml 3.06
letouzey
2010-05-19
Add (almost) compatibility with camlp4, without breaking support for camlp5
letouzey
2010-04-29
After the approval of Bruno, here the patch for the checker.
soubiran
2010-04-29
Remove the svn-specific $Id$ annotations
letouzey
2010-03-18
kills a warning about vo in checker/safe_typing
letouzey
2010-03-12
fixed confusion between number of cstr arguments and number of pattern variab...
barras
2010-02-19
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-01-08
* Segmenttree: New. A very simple implementation of segment trees.
regisgia
2009-12-20
* Rewrite [classify_unicode] using standard unicode tables.
regisgia
2009-12-01
fix coqchk options documentation
barras
2009-10-21
This big commit addresses two problems:
soubiran
2009-09-17
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-08-23
Fix a small oversight in checker commit 12288.
herbelin
2009-08-22
Transfers to checker ("let"s in inductive arities + Coq root read-only).
herbelin
2009-04-08
Some dead code removal + cleanups
letouzey
2009-03-20
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-02
porting r11900 11905 and 11953 to trunk
barras
2009-02-11
Report des revisions #11826, #11828 et #11829 de v8.2 vers trunk
notin
2009-01-18
Backporting from v8.2 to trunk:
herbelin
2009-01-06
Conversion du fichier 'revision' en un fichier .ml + correction d'un bug dans...
notin
2008-12-19
Nettoyage des variables Coq et amélioration de coqmktop. Les
notin
2008-10-15
Report des commits 11417 et 11437 de la v8.2
soubiran
2008-09-02
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-07-24
fixed loop in dependency fold of the checker
barras
2008-06-29
Lissage de la gestion des chemins de chargement de fichiers :
herbelin
2008-05-23
doc of coqchk + improved module cache and computation of module sets
barras
2008-05-22
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-20
also fixed conversion of the checker
barras
2008-05-12
Changement de stratégie vis à vis du commit 10859 sur la gestion des
herbelin
2008-05-07
fixed bug with aliases
barras
2008-05-06
checker deals with polymorphic constants and module aliases
barras
2008-04-27
Correction du bug des types singletons pas sous-type de Set
herbelin
2008-04-21
added the .vo checker (with independent Makefile)
barras
[prev]