coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	Term.dest* functions now raise specific DestKO exn instead of Invalid_argument	letouzey	2013-03-12
\| \| \| \| \| \| \| \| \| \|	Warning the ml code of plugins may have to be adapted after this. Concerning coq itself, I've done the adaptations, let's hope I've forgotten none. In practice, the number of changes are relatively low, and the code is quite cleaner this way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16271 85f007b7-540e-0410-9357-904b9bb8a0f7
*	More informative error when a global reference is used in a context of	herbelin	2013-02-28
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	local variables which is a different from the one of its definition. E.g.: Section A. Variable n:nat. Definition c:=n. Goal True. clear n. Check c. [I'm however unsure that "n" should not continue to be accessible via some global (qualified) name, even after the "clear n".] git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16256 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modulification of identifier	ppedrot	2012-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
*	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot	2012-09-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 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
*	Fixing vm_compute bug #2729 (function used to decompose constructors	herbelin	2012-03-13
\| \| \| \| \| \| \| \|	did not handle let-ins and was wrongly specified). Thanks to Pierre Boutillier and Pierre-Marie Pédrot for pointing out the source of the bug. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15027 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed bug #2105 (compilation of free de Bruijn) and missing lift of ↵	barras	2010-07-29
\| \| \| \| \| \|	predicate in branch read-back (2) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13350 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
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correcting a delta normalization bug in VM (checked by benjamin)	jforest	2008-09-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11423 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed bug #1780: a lift was missing (match predicate)	barras	2008-05-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11017 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient	herbelin	2008-04-01
\| \| \| \| \| \| \| \|	pas correctes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nettoyage de code en vue de la release. Plus de Warning: Unused	aspiwack	2007-12-18
\| \| \| \| \| \| \| \| \|	Variable, et plus de trucs useless qui traînaient par ma faute (y compris dans le noyau, la honte). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10388 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Processor integers + Print assumption (see coqdev mailing list for the	aspiwack	2007-05-11
\| \| \| \| \| \| \| \| \|	details). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9821 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection contre les warnings 'unused variable' de ocaml 3.09	herbelin	2007-01-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9503 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction du bug : VM value extraction error (PR#1290)	bgregoir	2006-11-29
\| \| \| \| \| \| \| \|	Benjamin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9406 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension du polymorphisme de sorte au cas des définitions dans Type.	herbelin	2006-10-28
\| \| \| \| \| \| \| \| \| \|	(suppression au passage d'un cast dans constant_entry_of_com - ce n'est pas normal qu'on force le type s'il n'est pas déjà présent mais en même temps il semble que ce cast serve pour rafraîchir les univers algébriques...) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9310 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Ajout d'un cast vm dans la syntaxe : x <: t	bgregoir	2006-07-22
	Part contre ces cas sont detruis dans les "Definition" (pas dans les "Lemma") je comprends pas ou ils sont enlev'e... Si une id'ee ... - Correction d'un bug dans vm_compute plusieurs fois signal'e par Roland. - Meilleur compilation des coinductifs, on utilise maintenant vraimment du lazy. - Enfin un peu plus de doc dans le code de la vm. Benjamin git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9058 85f007b7-540e-0410-9357-904b9bb8a0f7