coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Keep structure information for Fixpoint declaration and Fix terms	bertot	2004-02-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5386 85f007b7-540e-0410-9357-904b9bb8a0f7
*	commit précédent erroné	herbelin	2004-02-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5366 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bugs/insuffisances trouvees en traduisant MMode	herbelin	2004-02-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5361 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- fixed the Assert_failure error in kernel/modops	barras	2004-02-18
\| \| \| \| \| \| \| \| \|	- fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation de qqs bugs du traducteur	barras	2004-01-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5248 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bugs avec Pose et Assert	barras	2004-01-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5190 85f007b7-540e-0410-9357-904b9bb8a0f7
*	certains id n'etaient pas renommes pour eviter les conflits avec les mots-cles	barras	2004-01-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5172 85f007b7-540e-0410-9357-904b9bb8a0f7
*	meilleure presentation des commentaires du traducteur	barras	2004-01-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5168 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Finalement, espacement autour du ':' pour a la fois exists, forall et fun	herbelin	2003-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5135 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modif existentielle (exists \| --> exists ,) + bug d'affichage des pt fixes	barras	2003-12-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5099 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Protection du nom Eval pour eviter conflit avec Eval in	herbelin	2003-12-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5097 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Rle_monotony_contra devenu Rmult_le_reg_l avant traduction	herbelin	2003-12-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5063 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommages de variables dans RIneq	herbelin	2003-11-29
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5021 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout de Znumtheory.v dans ZArith	letouzey	2003-11-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4952 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Distinction entre 'as _' qui cache le terme filtre (si variable) et rien ↵	herbelin	2003-11-19
\| \| \| \| \| \|	dans case_item git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4949 85f007b7-540e-0410-9357-904b9bb8a0f7
*	reparation bug moins unaire (erreur de PP)	barras	2003-11-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4944 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Automatisation de la traduction de iff_trans; renommage IF	herbelin	2003-11-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4903 85f007b7-540e-0410-9357-904b9bb8a0f7
*	moins unaire au niveau 35, tactiques simple_induction et simple_destruct, ↵	barras	2003-11-13
\| \| \| \| \| \|	Local devient Let git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4897 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place systeme de renommage des noms de variables liees dans la ↵	herbelin	2003-11-12
\| \| \| \| \| \|	bibliotheque standard git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4867 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petits changements de syntaxe	barras	2003-11-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4860 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Finalement, niveau 0 pour l'argument du '-' unaire, pour éviter que	herbelin	2003-11-01
\| \| \| \| \| \| \| \| \|	les entiers positifs soient parenthésés en tant qu'arguments de fonction; tant pis, il faudra écrire '-(-x)' au lieu de '--x' Ajout CPatNotation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4754 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des negatifs au niveau de l'application, et des positifs au dessus ↵	herbelin	2003-10-30
\| \| \| \| \| \|	du niveau du moins unaire git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4744 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
*	Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation ↵	herbelin	2003-10-21
\| \| \| \| \| \|	par Pptactic git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4694 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
*	Ajout printers pour constr et constr_pattern (sans traduction)	herbelin	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4569 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement nouvelle syntaxe (pt fixes)	barras	2003-10-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4559 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Des abbreviations pour constrintern.ml	herbelin	2003-10-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4546 85f007b7-540e-0410-9357-904b9bb8a0f7
*	as au niveau de app	herbelin	2003-10-02
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4516 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Syntaxe plus liberale pour le type des arguments de filtrage du 'match'	herbelin	2003-09-26
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4491 85f007b7-540e-0410-9357-904b9bb8a0f7
*	traducteur: affiche les commentaires a l'interieur des commandes	barras	2003-09-22
\| \| \| \| \| \| \|	extraction: pb avec les variables de section definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4450 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place d'implicites par noms en v8	herbelin	2003-09-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4430 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Niveau du 'as' des motifs	herbelin	2003-09-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4413 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pour appliquer les noms reserves aussi aux binders	herbelin	2003-09-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4404 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Mise en place affichage spécifique pour le scope des types	herbelin	2003-09-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4361 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage des projections au niveau 1	herbelin	2003-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4349 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pretty-pretting fix	herbelin	2003-09-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4340 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout If; protection contre clash dans return_type	herbelin	2003-09-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4330 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Paramétrisation vis à vis de existential_key	herbelin	2003-09-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4321 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Passage de lconstr à constr pour les arguments immédiat de commandes	herbelin	2003-09-06
\| \| \| \| \| \| \| \|	et tactiques; qqes bugs d'affichage; passage de la précédence des projections de 10 à 9 avec associativité à gauche git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4312 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affichage des 'fun' suivis de 'let' en utilisant explicitement un 'let'	herbelin	2003-09-03
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4300 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug et amliorations diverses	herbelin	2003-08-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4263 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle mouture du traducteur v7->v8	herbelin	2003-08-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Option -v8 à coqtop lance coqtopnew Le terminateur reste "." en v8 Ajout construction primitive CLetTuple/RLetTuple Introduction typage dans le traducteur pour traduire les Case/Cases/Match Ajout mutables dans RCases or ROrderedCase pour permettre la traduction Ajout option -no-strict pour traduire les "Set Implicits" en implicites stricts + Bugs ou améliorations diverses Raffinement affichage projections de Record/Structure. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4257 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Formattage pattern 'match'	herbelin	2003-06-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4200 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout notation c.(f) en v8 pour les projections de Record; raffinement divers	herbelin	2003-06-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4123 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Suppression définitive de lmatch et or_metanum dans tacinterp	herbelin	2003-05-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4054 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour ↵	herbelin	2003-05-21
\| \| \| \| \| \|	les metavariables de patterns; réparation local défs récursive dans ltac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4045 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage CMeta en CPatVar qui sert à saisir les PMeta de Pattern	herbelin	2003-05-19
\| \| \| \| \| \| \| \| \|	Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Separation entre les 2 propositions de syntaxe	herbelin	2003-05-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4004 85f007b7-540e-0410-9357-904b9bb8a0f7
*	coqide: toolbar/autosave	monate	2003-05-07
\| \| \| \| \| \| \| \| \|	Hugo: Suppression du type dans les notations == et <> entre Suppression du type dans les notations == et <> entre volution second traducteur selon discussion TYPES git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3993 85f007b7-540e-0410-9357-904b9bb8a0f7