coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Renommage de RealsB en Rbase	desmettr	2003-01-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3508 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Renommage de Rbase.v en RIneq.v	desmettr	2003-01-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3507 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-01-16
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3506 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Problème de désynchronisation des variables du type et du corps d'un ↵	herbelin	2003-01-15
\| \| \| \| \| \|	point-fixe git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3504 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à ↵	herbelin	2003-01-15
\| \| \| \| \| \|	une sorte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3503 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug en présence de let-in	herbelin	2003-01-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3502 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Nouvelle interprétation des nombres réels	desmettr	2003-01-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3499 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug en présence de let-in	herbelin	2003-01-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3498 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Syntaxe 'Record id : c ...' autorisée même si c n'est que convertible à ↵	herbelin	2003-01-15
\| \| \| \| \| \|	une sorte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3497 85f007b7-540e-0410-9357-904b9bb8a0f7
*	patch configure (V Aymeric)	filliatr	2003-01-13
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3496 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-01-10
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3495 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Export M + Module M <: SIG	coq	2003-01-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3494 85f007b7-540e-0410-9357-904b9bb8a0f7
*	correction de bug de Subst: ne faisait rien lorsque l'hypothese	barras	2003-01-09
\| \| \| \| \| \| \|	n'apparaissait que dans le but... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3493 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-01-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3492 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Retour printer ast pour V7.4	herbelin	2003-01-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3491 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2003-01-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3490 85f007b7-540e-0410-9357-904b9bb8a0f7
*	SearchAbout	filliatr	2003-01-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3489 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bit vectors	filliatr	2003-01-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3488 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration règles d'affichage	herbelin	2002-12-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3487 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Commentaires; optimisation	herbelin	2002-12-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3486 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Amélioration choix des noms dans abstract_list_all	herbelin	2002-12-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3485 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte notations dans les extensions de motiff	herbelin	2002-12-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3484 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Re-installation nombres dans les motifs sur Z	herbelin	2002-12-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3483 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Utilisation du second-ordre avec possibilité de K-rédex dans lemInv	herbelin	2002-12-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3482 85f007b7-540e-0410-9357-904b9bb8a0f7
*	code mort	herbelin	2002-12-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3481 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Re-essai de forcer le terme réécrit à apparaître dans le but	herbelin	2002-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3480 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Tentative d'interdire les K-abstractions si allow_K est faux et le	herbelin	2002-12-23
\| \| \| \| \| \| \|	motif n'a pas de métas (dans unify_to_subterm_list) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3479 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte application partielle dans dependent	herbelin	2002-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3478 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-12-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3477 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cas motif universel	herbelin	2002-12-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3476 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack sur la tentative d'interdire les K-abstractions dans l'unification	herbelin	2002-12-21
\| \| \| \| \| \| \|	faite par Rewrite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3475 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Légère amélioration des messages d'erreur des with-bindings et des Rewrite	herbelin	2002-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3474 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affinement affichage	herbelin	2002-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3473 85f007b7-540e-0410-9357-904b9bb8a0f7
*	code mort	herbelin	2002-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3472 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Affinement affichage	herbelin	2002-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3471 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plus de notation cablees dans 'annot'	herbelin	2002-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3470 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-12-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Prise en compte des coercions dans les 'with' bindings	herbelin	2002-12-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3468 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-12-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3464 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Petit netoyage dans lib	coq	2002-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3463 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression de l'archive cvs d'un bout de debug	letouzey	2002-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3462 85f007b7-540e-0410-9357-904b9bb8a0f7
*	les empty ind et les singletons etaient oublies par add_recursors	letouzey	2002-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3461 85f007b7-540e-0410-9357-904b9bb8a0f7
*	apres correction du probleme de Global.env, retour du mis_constr_nargs_env	letouzey	2002-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3460 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bug: Global.env() executé au chargement -> eta-expansion	letouzey	2002-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3459 85f007b7-540e-0410-9357-904b9bb8a0f7
*	simplification de solve_subgoal: n'utilise plus frontier	barras	2002-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite du commit precedent	barras	2002-12-19
\| \| \| \| \| \| \| \|	- amelioration des messages d'erreurs de la condition de garde - reorganisation de clenv.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3457 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj	filliatr	2002-12-19
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3456 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- amelioration des messages d'erreur de la condition de garde	barras	2002-12-18
\| \| \| \| \| \| \|	- restructuration de clenv.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3455 85f007b7-540e-0410-9357-904b9bb8a0f7
*	stupide inlining des construsteurs	letouzey	2002-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3454 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Contexte locale non-vide interdit a la fin d'un module ou module type	coq	2002-12-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3453 85f007b7-540e-0410-9357-904b9bb8a0f7