coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Update headers following #6543.	Théo Zimmermann	2018-02-27
\|
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
\|
*	Update copyright headers.	Maxime Dénès	2016-01-20
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Checker: regroup all vo-related types in cic.mli	letouzey	2013-04-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16398 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updating headers.	herbelin	2012-08-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)	letouzey	2011-10-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	When doing a [check_subtypes env mtb1 mtb2], we used to always add [mtb1] in the environment. But since the stricter checks of commit r14150, this is an error if the environment already knows [mtb1] (for instance when doing (F M) and checking that M is compatible with the type of the arg of F. [check_subtypes] now expect [mtb1] to be already in env, and we move the add_module to the unique call site of this function that requires it. Moreover, we solve a second issue : when subtyping a functor, we update the environment once inside the functor, and this is also refused by the checks of commits r14150. So we first remove the module name from the env before doing the update. Since the module added earlier was a functor, there is no inner defs to chase in env. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14615 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Checker: remove some dead code	letouzey	2010-09-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13462 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Updated all headers for 8.3 and trunk	herbelin	2010-07-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13323 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remove the svn-specific $Id$ annotations	letouzey	2010-04-29
\| \| \| \| \| \| \| \| \| \| \|	- 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
*	added the .vo checker (with independent Makefile)	barras	2008-04-21
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10826 85f007b7-540e-0410-9357-904b9bb8a0f7