aboutsummaryrefslogtreecommitdiff
path: root/checker/validate.ml
AgeCommit message (Collapse)Author
2016-01-20Update copyright headers.Maxime Dénès
2015-01-12Update headers.Maxime Dénès
2014-12-19Fixing performance issue of checker validation.Pierre-Marie Pédrot
The validation process was passing most of its time in the construction of the name of the current context.
2014-02-26fix checker w.r.t. Dyn.t validationEnrico Tassi
discrepancy introduced in commit 400327165edcba667ebb70ebb89052455656b719
2013-08-23Adding dynamic value printing to votour through a registering mechanism.ppedrot
TODO: register the desired dynamic types. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16733 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-08-09checker validation made a bit more verbosegareuselesinge
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16690 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-15Checker: vo validation checks the absence of Var/Evar/Metaletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16405 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-04-15Checker: reified encoding of .vo types in values.mlletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16399 85f007b7-540e-0410-9357-904b9bb8a0f7
2013-02-19Names: revised representation of constants and mutual_inductiveletouzey
- a module KernelPair for improving sharing between constant and mind - shorter representation than a pair when possible - exports comparisions on constant and mind and ... - a kn_equal function instead of Int.equal (kn_ord ...) 0 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16217 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-10-06still some more dead code removalletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15875 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Updating headers.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-03-26Adapt the checker after commit 15080letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15100 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-09-24Checker: remove some dead codeletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13462 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-30adpated the checker to handle coomutative cuts and lazynessbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13365 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-24Updated all headers for 8.3 and trunkherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
- Many of them were broken, some of them after Pierre B's rework of mli for ocamldoc, but not only (many bad annotation, many files with no svn property about Id, etc) - Useless for those of us that work with git-svn (and a fortiori in a forthcoming git-only setting) - Even in svn, they seem to be of little interest git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-19added validation of delta_resolver (which seem to have an impact on typing)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12800 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-02-19[checker] fixed vo validation problems, module incompatibilities remainbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12799 85f007b7-540e-0410-9357-904b9bb8a0f7
2009-03-02porting r11900 11905 and 11953 to trunkbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11954 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-26 16:43:24 +0000