coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	maj	coq	2005-01-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6542 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement de 'project' dans Refiner pour supprimer des dépendances en ↵	herbelin	2005-01-01
\| \| \| \| \| \|	Tacmach git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6541 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6539 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement de 'project' dans Refiner pour supprimer des dépendances en ↵	herbelin	2004-12-31
\| \| \| \| \| \|	Tacmach git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6538 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de la dépendance en Tacmach pour pouvoir être appelé de ↵	herbelin	2004-12-31
\| \| \| \| \| \|	top_printers sans tirer Tacred et les fichiers C de la machine virtuelle git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6537 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Compatibilité ancien nom de ocamldebug-coq	herbelin	2004-12-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6536 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement ocamldebug-v7 par lien symbolique ne marche pas, finalement, ↵	herbelin	2004-12-31
\| \| \| \| \| \|	création du lien par configure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6535 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement ocamldebug-v7 par ocamldebug-coq (2ème)	herbelin	2004-12-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6534 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6531 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ↵	herbelin	2004-12-30
\| \| \| \| \| \|	réduit aussi les types du contexte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6530 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6528 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6527 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ExtraRedExpr maintenant sans argument: pas très souple mais au moins ↵	herbelin	2004-12-29
\| \| \| \| \| \|	convient pour l'exemple de MapleMode qui lui ne passait pas quand un argument était exigé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6526 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug control_only_guard	herbelin	2004-12-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6524 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout printer bigint	herbelin	2004-12-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6523 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug transformation assert dans commit précédent	herbelin	2004-12-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6522 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6518 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6516 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6515 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)	herbelin	2004-12-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6514 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout test bug 860	herbelin	2004-12-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6513 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement du coeur d'omega (omega.ml) par la version plus générale ↵	herbelin	2004-12-27
\| \| \| \| \| \|	utilisée par romega (omega2.ml, qui, à l'occassion, disparaît sous ce nom) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6512 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement du coeur d'omega (omega.ml) par la version plus gnrale utilise ↵	herbelin	2004-12-27
\| \| \| \| \| \|	par romega (omega2.ml, qui, l'occassion, disparat sous ce nom) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6511 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6509 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6507 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6506 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage d'une bibliothèque de grands entiers naturels vers une ↵	herbelin	2004-12-25
\| \| \| \| \| \|	bibliothèques de grands entiers relatifs munis des 4 opérations de base git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6505 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage d'une bibliothèque de grands entiers naturels vers une ↵	herbelin	2004-12-25
\| \| \| \| \| \|	bibliothèques de grands entiers relatifs munis des 4 opérations de base git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6504 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6502 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage d'une bibliothèque de grands entiers naturels vers une ↵	herbelin	2004-12-24
\| \| \| \| \| \|	bibliothèques de grands entiers relatifs munis des 4 opérations de base git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6501 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2004-12-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6500 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage d'une bibliothèque de grands entiers naturels vers une ↵	herbelin	2004-12-24
\| \| \| \| \| \|	bibliothèques de grands entiers relatifs munis des 4 opérations de base git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6499 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6497 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ coq v8	herbelin	2004-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6496 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ coq v8	herbelin	2004-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6495 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage de ocamldebug-v7 en ocamldebug-coq (pour passage à la v8)	herbelin	2004-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6494 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage de ocamldebug-v7 en ocamldebug-coq (pour passage à la v8	herbelin	2004-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6493 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6491 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mecanisme d'affichage des types (notamment les conclusions des buts) ↵	herbelin	2004-12-22
\| \| \| \| \| \|	typiquement pour eviter les coercions en tete git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6490 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6488 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6486 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6484 85f007b7-540e-0410-9357-904b9bb8a0f7
*	In_dec transparent (wish #902)	herbelin	2004-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6483 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6481 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6479 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6477 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6475 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6473 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6471 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	coq	2004-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6469 85f007b7-540e-0410-9357-904b9bb8a0f7