coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add a parameter to QuestionMark evar kind to say it can be turned into an obl...	msozeau	2007-03-19
*	Un chouia de portabilité en plus et pas de test si pas de bogomips	herbelin	2007-03-19
*	MAJ test complexité pour considérer le cas d'un temps avec un nombre	herbelin	2007-03-17
*	Correction du bug #1441	notin	2007-03-16
*	r11153@tannat: jforest \| 2007-03-16 10:25:55 +0100	jforest	2007-03-16
*	Test de non-régression pour commit 9673	herbelin	2007-03-15
*	Typos	herbelin	2007-03-15
*	Suppression argument pattern_source du case_info (code jamais utilisé)	herbelin	2007-03-15
*	Prévention notations récursives sans terminal à gauche et qui font boucler	herbelin	2007-03-15
*	Add destruct_call variant where naming of introduced hypotheses is possible. ...	msozeau	2007-03-15
*	Add destruct_call_concl in SubtacTactics and fix obvious obligation handling ...	msozeau	2007-03-14
*	Bug dans Makefile (COQINSTALLPREFIX)	notin	2007-03-14
*	Removed an unnecessary argument (p : positive) in Prect_base.	emakarov	2007-03-14
*	Solve obligation handling bug of trying to solve automatically at Next Obliga...	msozeau	2007-03-13
*	Correction bug #1439 (comportement de replace by)	notin	2007-03-13
*	Proof simplification for eq_nat_dec et le_lt_dec: induction over	letouzey	2007-03-12
*	correction du bug 1432	jforest	2007-03-11
*	Remove bugguy notations	msozeau	2007-03-11
*	bug#1434 importing fonctor arguments, now it works.	soubiran	2007-03-09
*	Create a program_scope in subtac Utils	msozeau	2007-03-08
*	Add Program keywords to coqwc	msozeau	2007-03-08
*	Transparence de eq_dec et lt_dec daans OrderedTypeFacts	notin	2007-03-08
*	Application suggestion #1430 de Yevgeniy pour TEXINPUTS	herbelin	2007-03-07
*	màj dépendances .v: SubtacTactics.vo	lmamane	2007-03-06
*	FSetInterface: new item choose_equal in the spec S (request of P. Casteran)	letouzey	2007-02-28
*	The right tactics for definitions using measures.	msozeau	2007-02-28
*	Fix wf bug from F. Besson and work on ineqs generation.	msozeau	2007-02-27
*	Revision of the coqide configuration:	letouzey	2007-02-27
*	Correction d'un bug de l'install (win)	notin	2007-02-27
*	Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...	herbelin	2007-02-24
*	Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)	herbelin	2007-02-24
*	Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)	herbelin	2007-02-24
*	Améliorations utiles pour les Makefile répartis sur plusieurs répertoires	herbelin	2007-02-24
*	Opacity parameterization for obligations working.	msozeau	2007-02-24
*	Debug wellfounded defs, work on cleaning obls envs	msozeau	2007-02-23
*	Ajout fonction clenv_conv_leq pour résoudre les pbs de la forme	herbelin	2007-02-22
*	Échange des mots clés 'using' et 'with' en argument de 'firstorder' (wish #...	notin	2007-02-22
*	doc: typo/english: "is left associating" -> "is left-associative".	lmamane	2007-02-22
*	Documentation of tactical "t1 \|\| t2": t2 is executed if t1 fails to	lmamane	2007-02-22
*	Utilisation de l'environnement pour l'affichage de certains messages d'erreurs	herbelin	2007-02-21
*	Correction typo liée au commit 8779 (levait une anomalie)	herbelin	2007-02-21
*	Prise en compte de l'environnement dans les pbs de conversion + MAJ CHANGES	herbelin	2007-02-21
*	Removed some useless code in mod_typing that was redundant with safe_typing.	soubiran	2007-02-21
*	Fixed the pseudo-cicularity problem due to the with operator on Module Type.	soubiran	2007-02-21
*	Correct coq depend, add eq_rect elimination tactic to SubtacTactics	msozeau	2007-02-19
*	Ajouts de lemmes dans Min et Max	notin	2007-02-19
*	Various little subtac fixes, add some useful tactics.	msozeau	2007-02-19
*	Compilation de la FAQ	notin	2007-02-18
*	Add subtac keywords to coqide and coqdoc, add 'dec' as keyword in subtac Utils.	msozeau	2007-02-16
*	Add 'dest obj as pat in body' keyword as a pattern-matching shortcut.	msozeau	2007-02-16