coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	petits changements cosmetiques sur les tactiques	barras	2002-02-15
\| \| \| \| \| \| \| \|	+ Clear independant de l'ordre des hypotheses, et substituant les hypotheses definies git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2481 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suite et fin (?) de haskell: gestion des modules, mise en place du'un test	letouzey	2002-02-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2480 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bootstrap consistent avec les options de la ligne de commande	filliatr	2002-02-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2478 85f007b7-540e-0410-9357-904b9bb8a0f7
*	debut de gestion des open pour extraction modulaire	letouzey	2002-02-15
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2477 85f007b7-540e-0410-9357-904b9bb8a0f7
*	qq inline manuels (sigS_rec ...) + utilisation de library_part	letouzey	2002-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2476 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Reforme de la gestion des args recursifs (via arbres reguliers)	barras	2002-02-14
\| \| \| \| \| \| \|	- coqtop -byte -opt bouclait! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2475 85f007b7-540e-0410-9357-904b9bb8a0f7
*	option -dump-glob pour coqdoc	filliatr	2002-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2474 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Syntaxe IF then else au lieu de either and_then or_else	barras	2002-02-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2473 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Raffinement library_part	herbelin	2002-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2472 85f007b7-540e-0410-9357-904b9bb8a0f7
*	petite modif pour ne pas expanser trop de let pendant l'unification	barras	2002-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2471 85f007b7-540e-0410-9357-904b9bb8a0f7
*	suppression de la condition de la permutation case/fun	letouzey	2002-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2470 85f007b7-540e-0410-9357-904b9bb8a0f7
*	pretty print	letouzey	2002-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2469 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test & correction de la production de code Haskell	letouzey	2002-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2468 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout library_part	herbelin	2002-02-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2467 85f007b7-540e-0410-9357-904b9bb8a0f7
*	substitution et pattern modulo let	barras	2002-02-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2466 85f007b7-540e-0410-9357-904b9bb8a0f7
*	bad printing of Zeta reduction flags (was missing)	barras	2002-02-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2465 85f007b7-540e-0410-9357-904b9bb8a0f7
*	mauvais comportement de l'inversion vis-a-vis des lets	barras	2002-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2464 85f007b7-540e-0410-9357-904b9bb8a0f7
*	prterm -> prterm_env	filliatr	2002-02-08
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2463 85f007b7-540e-0410-9357-904b9bb8a0f7
*	affichages avec prterm_env et non prterm; deb_print pour vraiment ne rien ↵	filliatr	2002-02-08
\| \| \| \| \| \|	faire si pas debug git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2462 85f007b7-540e-0410-9357-904b9bb8a0f7
*	erreur mineure dans le test des inductifs imbriques	barras	2002-02-07
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2461 85f007b7-540e-0410-9357-904b9bb8a0f7
*	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