coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	correction Abstract (et make world passe!)	filliatr	2000-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@794 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression des (* open Generic *)	filliatr	2000-11-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- simplification Makefile (compilation des fichiers .ml'; pas encore parfait	filliatr	2000-10-31
\| \| \| \| \| \| \| \|	car on passe par les fichiers .ml) - Require Export enfin rétabli avec la bonne sémantique git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@792 85f007b7-540e-0410-9357-904b9bb8a0f7
*	.old virés (CVS est là pour ca)	filliatr	2000-10-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@791 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un switch pour le debugger	delahaye	2000-10-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@790 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression d'Intuition (trop intelligent?)	delahaye	2000-10-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@789 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pour eviter temporairement le "Auto with zarith"	delahaye	2000-10-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@788 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement de Tauto et Intuition	delahaye	2000-10-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@787 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tactiques utilisateur + debugger	delahaye	2000-10-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@786 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Priorite du Try/Orelse + Debug switch + correction bug dans Pattern	delahaye	2000-10-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@785 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pour le Require Export (temporaire)	delahaye	2000-10-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@784 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajouts pour les tactiques utilisateur	delahaye	2000-10-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@783 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2000-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@782 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Clarification message d'erreur	herbelin	2000-10-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@781 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2000-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@780 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage command -> constr	herbelin	2000-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@779 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Simpl fait trop maintenant; faut adapter	herbelin	2000-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@778 85f007b7-540e-0410-9357-904b9bb8a0f7
*	erreur dans intro_gen corrigée	filliatr	2000-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@777 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Chasse au Cast de Cast	herbelin	2000-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@776 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Intro choue si le nom d'hypothse existe au lieu de mettre un avertissement	herbelin	2000-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@775 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajoute : Ast dans la regle de grammaire	mayero	2000-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@774 85f007b7-540e-0410-9357-904b9bb8a0f7
*	g_natsyntax et g_zsyntax maintenant toujours linkes	filliatr	2000-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@773 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise a jour TheoryList	mohring	2000-10-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@772 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2000-10-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@771 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Essai de remplacement du whd_betaiotaevar de Qed par un whd_ise	herbelin	2000-10-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@770 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression cas Cast dans whd_ise et whd_ise1; Suppression du cast au moment ↵	herbelin	2000-10-26
\| \| \| \| \| \|	de l'instanciation des Meta dans plain_instance git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@769 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Require Export recursifs	filliatr	2000-10-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@768 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Semi_Ring_Theory_of decommente	mohring	2000-10-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@767 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retire les parentheses autour des tactiques	mohring	2000-10-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@766 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout de la mthode load_function pour exporter les 'tactic-ring-theory'	herbelin	2000-10-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@765 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug Simpl avec Cases cache sous plusieurs constantes	herbelin	2000-10-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@764 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage var en named et decl en assum	herbelin	2000-10-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@763 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ntrefiner.ml* removed in module xml	sacerdot	2000-10-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@762 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Manquait le cas Constr de dyn_polynom	herbelin	2000-10-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@761 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug pop_path_prefix : List.rev manquant	herbelin	2000-10-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@760 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Porting from V6 finished, but not working.	sacerdot	2000-10-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@759 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Added xml contribution to configure	sacerdot	2000-10-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@758 85f007b7-540e-0410-9357-904b9bb8a0f7
*	xml contribution added to the Makefile	sacerdot	2000-10-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@757 85f007b7-540e-0410-9357-904b9bb8a0f7
*	xml contribution created.	sacerdot	2000-10-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@756 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2000-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@755 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Changement des analyseurs syntaxiques de Grammar et Syntax	herbelin	2000-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@754 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un espace	herbelin	2000-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@753 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Syntaxe des tactiques	herbelin	2000-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@752 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage command -> constr et changement des analyseurs syntaxiques de ↵	herbelin	2000-10-24
\| \| \| \| \| \|	Grammar et Syntax git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@751 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug réduction suite modifs let-in	herbelin	2000-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@750 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Meilleur endroit pour déclarer les parseurs de grammaires et joli affichage	herbelin	2000-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@749 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug de copier-coller	herbelin	2000-10-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@748 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ	herbelin	2000-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@747 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Modifications pour implicites améliorés	herbelin	2000-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@746 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rétablissement compatibilité des implicites (2ème) (mais amélioration)	herbelin	2000-10-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@745 85f007b7-540e-0410-9357-904b9bb8a0f7