aboutsummaryrefslogtreecommitdiff
path: root/checker/check.ml
AgeCommit message (Collapse)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-01-18Backporting from v8.2 to trunk:herbelin
- Filtering of doc compilation messages (11793,11795,11796). - Fixing bug #1925 and cleaning around bug #1894 (11796, 11801). - Adding some tests. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11802 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-09-02fixed bug #1927 + univ constraints (module cstrs include cstrs of its ↵barras
subcomponents) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11348 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-07-24fixed loop in dependency fold of the checkerbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11256 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-29Lissage de la gestion des chemins de chargement de fichiers :herbelin
- Option -R fait maintenant des Import à tous les niveaux de la hiérarchie de répertoires. Par exemple, Require "Init.Wf" marche. - Option -I rend maintenant possible l'accès aux sous-répertoires via les noms qualifiés. Ainsi -R est exactement comme -I sauf qu'il rend récursivement visibles les noms non qualifiés. - Ajout option -I dir -as coqdir, et par symétrie, -R dir -as coqdir. - Ajout option -exclude-dir pour exclure certains sous-répertoires de la descente récursive de -R. - Amélioration message de localisation pour fichiers venant d'un "state". - Adaptation du checker (et ajout du test check_coq_overwriting qui semblait involontairement oublié dans l'option -R). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11188 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-23doc of coqchk + improved module cache and computation of module setsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10979 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-07fixed bug with aliasesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10896 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-05-06checker deals with polymorphic constants and module aliasesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10892 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-04-21added the .vo checker (with independent Makefile)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10826 85f007b7-540e-0410-9357-904b9bb8a0f7