coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Ajout option -v8 à coqtopnew pour permettre le changement de comportement ↵	herbelin	2003-04-09
\| \| \| \| \| \|	des implicites (passage au mode strict) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3882 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"	herbelin	2003-04-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3881 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Alignement du comportement des implicites d'inductif en sortie de section ↵	herbelin	2003-04-09
\| \| \| \| \| \|	sur celui des constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3880 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage K; equivalence JMeq et eq_dep sur Type	herbelin	2003-04-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3879 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Defined	herbelin	2003-04-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3878 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import".	herbelin	2003-04-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3877 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression de l'étage "Import nat/Z/R_scope". "Open Scope" remplace "Import"	herbelin	2003-04-09
\| \| \| \| \| \| \|	Expérience avec les notations et les scopes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3876 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réorganisation de Impargs + mise en place d'une infrastructure	herbelin	2003-04-09
\| \| \| \| \| \| \| \|	(notatemment des tables de parsing et d'affichage différenciées) permettant au traducteur de changer les implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3875 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réorganisation de Impargs + mise en place d'une infrastructure	herbelin	2003-04-09
\| \| \| \| \| \| \| \|	(notatemment des tables de parsing et d'affichage différenciées) permettant au traducteur de changer les implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3874 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte affichage coercions traducteur dans Constrextern	herbelin	2003-04-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3873 85f007b7-540e-0410-9357-904b9bb8a0f7
*	on repasse aussi -thread a Caml	filliatr	2003-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3872 85f007b7-540e-0410-9357-904b9bb8a0f7
*	test: un boolean et une fonction check_for_interrupt inseree dans la ↵	filliatr	2003-04-08
\| \| \| \| \| \|	conversion pour permettre a Coq IDE d'interrompre Coq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3871 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des variables de grammaires de tactiques et dédollarisation ↵	herbelin	2003-04-08
\| \| \| \| \| \|	des metaident git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3870 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Application de l'absence d'export aux modules	herbelin	2003-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3869 85f007b7-540e-0410-9357-904b9bb8a0f7
*	En-tete doc	herbelin	2003-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3868 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout option "Local" à "Open Scope"	herbelin	2003-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3867 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-04-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3866 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des tactiques en v8	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3865 85f007b7-540e-0410-9357-904b9bb8a0f7
*	lconstr pour genterm en v8	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3864 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout translate	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3863 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Typo	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3862 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nommage explicite des hypotheses introduites quand le nom existe aussi comme ↵	herbelin	2003-04-07
\| \| \| \| \| \|	global git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3861 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Globalisation tactiques	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3860 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mauvaise resolution conflit dans commit precedent	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3859 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
\| \| \| \| \| \| \| \| \|	pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3858 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Globalisation des noms de tactiques dans les définitions de tactiques	herbelin	2003-04-07
\| \| \| \| \| \| \| \| \|	pour compatibilité avec les modules. Globalisation partielle des invocations de tactiques hors définitions (partielle car noms des Intros/Assert/Inversion/... non connus). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3857 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Stratégie d'affichage des coercions plus défensive (mais pas très optimale)	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3856 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cosmetique	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3855 85f007b7-540e-0410-9357-904b9bb8a0f7
*	code mort	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3854 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Espaces superflus	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3853 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage unicite/unicity pour la v8	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3852 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Aérer les := et : de "assert"	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3851 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout cas Match	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3850 85f007b7-540e-0410-9357-904b9bb8a0f7
*	BEST redondant	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3849 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression des explicitations d'implicite inutiles	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3848 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation de CAppExpl au lieu de CRef pour les hints pour qu'aucun implicite	herbelin	2003-04-07
\| \| \| \| \| \| \|	ne s'insére pour les références dont tous les arguments sont implicites git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3847 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Options d'affichage maintenant dans Constrextern	herbelin	2003-04-07
\| \| \| \| \| \| \|	Ajout "Set/Unset Printing Implicits" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3846 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Options d'affichage maintenant dans Constrextern	herbelin	2003-04-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3845 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-04-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3844 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Documentation, généralisation à eq sur Type, preuves d'équivalence des	herbelin	2003-04-03
\| \| \| \| \| \| \|	4 axiomes (K, UIP, eq_rec_eq, eq_dep_eq) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3843 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack du commit de Christine, qui posait probleme avec FTC	letouzey	2003-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3842 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Légères simplifications code de Field; message d'erreur si pas égalité	herbelin	2003-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3841 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-04-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3840 85f007b7-540e-0410-9357-904b9bb8a0f7
*	espace manquant	herbelin	2003-04-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3839 85f007b7-540e-0410-9357-904b9bb8a0f7
*	remplace == par = dans la tactique field pour que le debugger marche a ↵	narboux	2003-04-01
\| \| \| \| \| \|	nouveau apres suppression de == par hugo git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3837 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-04-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3836 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Déplacement with_option dans Options	herbelin	2003-04-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3835 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug #261 + amélioration nommage	herbelin	2003-04-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3834 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Extension de Replace aux égalités entre preuves	herbelin	2003-04-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3833 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fail 1 pour traverser le match	herbelin	2003-04-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3832 85f007b7-540e-0410-9357-904b9bb8a0f7