coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	petit nettoyage de kernel/inductive	barras	2002-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2460 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression du retour chariot a la fin de print_pure_constr	barras	2002-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2459 85f007b7-540e-0410-9357-904b9bb8a0f7
*	un assert false de trop (MLexn peut avoir des args)	letouzey	2002-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2458 85f007b7-540e-0410-9357-904b9bb8a0f7
*	oubli	letouzey	2002-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2457 85f007b7-540e-0410-9357-904b9bb8a0f7
*	gros changement dans mlutil.ml: ajout d'une elimination globale des prop	letouzey	2002-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2456 85f007b7-540e-0410-9357-904b9bb8a0f7
*	affichage des messages d'erreur pour Stack_overflow, Out_of_memory, Break	barras	2002-02-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2455 85f007b7-540e-0410-9357-904b9bb8a0f7
*	evaluable_constant retournait vrai pour les constantes opaques, ce qui faisait	barras	2002-02-05
\| \| \| \| \| \| \|	boucler la condition de garde git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2454 85f007b7-540e-0410-9357-904b9bb8a0f7
*	exclusion des rertoires de test de l'extraction	letouzey	2002-02-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2453 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'optimisations locales kill_prop	letouzey	2002-02-05
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2452 85f007b7-540e-0410-9357-904b9bb8a0f7
*	exceptionmal ratrappee	barras	2002-02-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2451 85f007b7-540e-0410-9357-904b9bb8a0f7
*	maj newsyntax	barras	2002-02-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2450 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout tactiques Rename et Pose; modifications pour Inversion	herbelin	2002-02-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2449 85f007b7-540e-0410-9357-904b9bb8a0f7
*	adaptation de l'extraction aux changements de Christine concernant rec/rect ↵	letouzey	2002-01-31
\| \| \| \| \| \|	et False_rec git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2448 85f007b7-540e-0410-9357-904b9bb8a0f7
*	changement generation de schema d'elimination, False_rec est primitif, ↵	mohring	2002-01-31
\| \| \| \| \| \|	Constructor tac git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2447 85f007b7-540e-0410-9357-904b9bb8a0f7
*	extraction des CoInductives via les Lazy d'ocaml	letouzey	2002-01-31
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2446 85f007b7-540e-0410-9357-904b9bb8a0f7
*	cosmetique	herbelin	2002-01-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2445 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ajout list_split3, pr_semicolon et pr_bar	herbelin	2002-01-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2444 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reparation erreur de syntaxe	mohring	2002-01-30
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2443 85f007b7-540e-0410-9357-904b9bb8a0f7
*	modification de la definition des def inductives unitaires et autorisation ↵	mohring	2002-01-29
\| \| \| \| \| \|	d'elimination sur la sorte Type git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2442 85f007b7-540e-0410-9357-904b9bb8a0f7
*	condition de positivite moins stricte vis-a-vis des parametres (cf bug de ↵	barras	2002-01-29
\| \| \| \| \| \|	Eduardo) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2441 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test affichage O de nat dans une expression sur Z	herbelin	2002-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2440 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug affichage de O (de nat) dans une expression sur Z	herbelin	2002-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2439 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2002-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2438 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Zdiv et Zmod dans Zcomplements	filliatr	2002-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2437 85f007b7-540e-0410-9357-904b9bb8a0f7
*	patch Omega (bug 129)	filliatr	2002-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2436 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction bug 'Check [b]if b then O else O'	herbelin	2002-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2435 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement cut_intro par true_cut_anon pour Inversion	herbelin	2002-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2434 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug calcul de la signature incorrecte en présence de letin	herbelin	2002-01-25
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2433 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction de l'ordre des open (sachant que de toutes façons, un	herbelin	2002-01-24
\| \| \| \| \| \| \| \|	Require au milieu d'un module sera considéré comme situé au début du module chargé) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2432 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Remplacement cut_intro par true_cut_anon	herbelin	2002-01-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2431 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug calcul de la signature incorrecte en présence de letin	herbelin	2002-01-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2430 85f007b7-540e-0410-9357-904b9bb8a0f7
*	code mort	herbelin	2002-01-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2429 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Cas LetIn superflu dans check_construct car normalisation préalable	herbelin	2002-01-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2428 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug dépendances en les corps des let-in oubliées	herbelin	2002-01-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2427 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Réparation bug 'known_dependent'	herbelin	2002-01-24
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2426 85f007b7-540e-0410-9357-904b9bb8a0f7
*	In Pcoq, the search commands had an erroneous behavior. Bound variables	bertot	2002-01-23
\| \| \| \| \| \| \| \|	in theorems were renamed to avoid the names present in the current goal's context. This version corrects this problem. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2425 85f007b7-540e-0410-9357-904b9bb8a0f7
*	paquet Debian 7.2-3	courant	2002-01-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2424 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mise a jour	filliatr	2002-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2423 85f007b7-540e-0410-9357-904b9bb8a0f7
*	warning en mode verbeux seulement	filliatr	2002-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2422 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction de Pierre Crégut pour le bug MERGE_EQ	herbelin	2002-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2421 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout test de Pierre Crégut	herbelin	2002-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2420 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Zinv -> Zopp	filliatr	2002-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2419 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2002-01-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2418 85f007b7-540e-0410-9357-904b9bb8a0f7
*	* empty log message *	herbelin	2002-01-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2417 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug MERGE_EQ	herbelin	2002-01-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2416 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Bug commentaire (i i)	herbelin	2002-01-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2415 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pas d'assert false dans un try with !	herbelin	2002-01-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2414 85f007b7-540e-0410-9357-904b9bb8a0f7
*	amadouage de coqweb	letouzey	2002-01-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2413 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plusieurs arguments autorisés pour Require et Read Module	herbelin	2002-01-18
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2412 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Plusieurs arguments autorisés pour Require et Read Module; mise en place ↵	herbelin	2002-01-18
\| \| \| \| \| \|	d'un mécanisme pour se souvenir de l'ordre des Open (mais pas activé); suppression du champ string dans le summary REQUIRE git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2411 85f007b7-540e-0410-9357-904b9bb8a0f7