coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Oubli d'un Set Implicit Arguments	herbelin	2003-11-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4825 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Biblio standard sans mention de la possibilite d'etre impredicatif	herbelin	2003-11-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4823 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Biblio standard sans impredicativite	herbelin	2003-11-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4822 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Des oublis	herbelin	2003-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4819 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Report des definitions sorties de fast_integer pour compatibilite	herbelin	2003-11-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4818 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Notations	herbelin	2003-11-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4816 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout répertoire NArith pour l'arithmétique binaire sur les nombres ↵	herbelin	2003-11-05
\| \| \| \| \| \|	positifs et naturels git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4809 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Preuve de l'incoherence de {A}+{~A} avec Set impredicatif	herbelin	2003-11-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4808 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Redondances	herbelin	2003-11-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4806 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restructuration ZArith et déport de la partie sur 'positive' dans NArith, ↵	herbelin	2003-11-05
\| \| \| \| \| \|	de la partie Omega dans contrib/omega git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4801 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Exporting ^; utilisation arg scope implicite	herbelin	2003-11-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4783 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cosmetique	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4780 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renforcement significatif du resultat principal	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4779 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rien de bien important	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4778 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Commentaires	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4777 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4774 85f007b7-540e-0410-9357-904b9bb8a0f7
*	AC + EXT -> EM	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4772 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Relations entre le choix (forme relationnelle) avec restriction ou non	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4771 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage bool en boolP pour eviter la qualification	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4770 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restauration preference Rge a Rle pour compatibilite...	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4769 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Restauration preference Rge a Rle pour compatibilite...; petit nettoyage	herbelin	2003-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4768 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les ↵	herbelin	2003-11-01
\| \| \| \| \| \|	entiers positifs soient parentheses en tant qu'arguments de fonction; tant pis, il faudra ecrire '-(-x)' au lieu de '--x' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4751 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Finalement, niveau 0 pour l'argument du '-' uniare, pour eviter que les ↵	herbelin	2003-11-01
\| \| \| \| \| \|	entiers positifs soient parentheses en tant qu'arguments de fonction; tant pis, il faudra ecrire '-(-x)' au lieu de '--x'; suppression notations - et / unaire en V7 pour compatibilite V7.4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4750 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Parsing du moins unaire au niveau de l'application qui n'a pas besoin d'etre ↵	herbelin	2003-10-30
\| \| \| \| \| \|	associative a gauche; gestion du signe dans le parseur pas dans l'interpreteur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4745 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Choix sous sa forme relationnelle	herbelin	2003-10-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4741 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ordre (symbolique) des Require	herbelin	2003-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4738 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage de la notations de paire dans core_scope	herbelin	2003-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4737 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage des notations de type dans type_scope	herbelin	2003-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4736 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout %core; MAJ niveau connecteurs logique	herbelin	2003-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4732 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2003-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4725 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fichier offrant l'axiome du choix unique en presence de logique classique	herbelin	2003-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4724 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fichier offrant l'axiome du choix en presence de logique classique	herbelin	2003-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4723 85f007b7-540e-0410-9357-904b9bb8a0f7
*	La logique sur Type inclut celle sur Set	herbelin	2003-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4722 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retour en arriere sur d'autres renommages de variables	herbelin	2003-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4721 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retour a un nommage non standard des variables pour compatibilite; report ↵	herbelin	2003-10-27
\| \| \| \| \| \|	'relation' pour compatibilite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4720 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug du commit precedent	herbelin	2003-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4716 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Commentaires	herbelin	2003-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4709 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation/Structuration	herbelin	2003-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4702 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation/Structuration	herbelin	2003-10-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4701 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reorganisation des niveaux (ex: = est a 70)	barras	2003-10-22
\| \| \| \| \| \| \|	Hint Destruct: syntaxe similaire aux autres hints... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4696 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Redondance de dec_eq_nat	herbelin	2003-10-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4692 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Type relation dans Datatypes	herbelin	2003-10-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4691 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Maintenant avant Datatypes	herbelin	2003-10-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4681 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajouts	herbelin	2003-10-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4680 85f007b7-540e-0410-9357-904b9bb8a0f7
*	R passe dans Set !	herbelin	2003-10-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4677 85f007b7-540e-0410-9357-904b9bb8a0f7
*	20 est uniquement associatif a gauche	herbelin	2003-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4672 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Des implicites plus 'naturels' pour eq_ind, identity_ind and co	herbelin	2003-10-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4669 85f007b7-540e-0410-9357-904b9bb8a0f7
*	nouvelle syntaxe de ltac	barras	2003-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4661 85f007b7-540e-0410-9357-904b9bb8a0f7
*	lettac -> set	barras	2003-10-16
\| \| \| \| \| \| \|	suppression de la notation carre de R git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4659 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Syntax error	herbelin	2003-10-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4653 85f007b7-540e-0410-9357-904b9bb8a0f7