coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Correction boucle du parseur en cas de caractÃère non unicode	herbelin	2006-11-20
*	Suppression du type 'tac dans les abstract_argument_type: devenu inutile	herbelin	2006-11-20
*	Dépendance inutile en Tacexpr, de proofs, qui se compile en principe après	herbelin	2006-11-19
*	mult_sym, plus_sym -> mult_comm, plus_comm	herbelin	2006-11-19
*	MAJ	herbelin	2006-11-19
*	Raffinement de l'unification de "apply": mémorisation de certains	herbelin	2006-11-19
*	Code mort (duplication de code dans reductionops.ml)	herbelin	2006-11-18
*	The emacs-U option now does not output any char above 250.	courtieu	2006-11-17
*	Small fix in functional graph merging.	courtieu	2006-11-16
*	suppression de code mort (avec bug de nom)	letouzey	2006-11-16
*	pb avec r9379 + modifs dans ring	barras	2006-11-16
*	Work on dep types pattern matching	msozeau	2006-11-16
*	suite de r9362: reconnaissance de qqs injections entre nat, N et Z	barras	2006-11-16
*	Adaptation à FreeBSD	notin	2006-11-16
*	Some usability enhancements.	msozeau	2006-11-15
*	Better solve using tactics impl.	msozeau	2006-11-13
*	Correction de la seconde partie du bug #1278	jforest	2006-11-13
*	Correction de la premiere partie du #1278 (but non referme en cas d'echec)	jforest	2006-11-13
*	Corrige un bug de calcul du temps effectif cquand la dernière décimale est 0	herbelin	2006-11-13
*	Encore des _sym au lieu de _comm	herbelin	2006-11-13
*	Correction typo	herbelin	2006-11-13
*	Fichiers obsolètes	herbelin	2006-11-11
*	Typo + ajout Qcanon.v	herbelin	2006-11-11
*	Ajout de dépliage de l'énoncé, si besoin est, dans apply in	herbelin	2006-11-10
*	generalisation de ring pour faire Ring_nf	barras	2006-11-10
*	Work on mutual defs, various bug fixes.	msozeau	2006-11-10
*	Correction d'un bug refine	herbelin	2006-11-10
*	Work on pattern inequalities for pattern matching branches.	msozeau	2006-11-10
*	Support for mutual defs in obligation handling.	msozeau	2006-11-09
*	Changement des modifeurs par défaut dans CoqIDE (problème de compatibilité...	notin	2006-11-07
*	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9348 85f007b7-540e-04...	filliatr	2006-11-07
*	Changement du magic number	notin	2006-11-06
*	fixes PR#1269 about function: there is no reason well founded induction is	bertot	2006-11-05
*	Suppression source de complexité polynomiale introduite par le polymorphisme	herbelin	2006-11-03
*	bug test complexité	herbelin	2006-11-03
*	gestion speciale du niveau 5 des ltac	barras	2006-11-02
*	Add doc on obligation solving commands.	msozeau	2006-11-02
*	Quick hack to solve to complexity issue in function mark_occur	herbelin	2006-11-01
*	Ajout test setoid_rewrite (cf bug #1176); anglicisation	herbelin	2006-11-01
*	Debug obligation handling code	msozeau	2006-10-31
*	Retour sur la modification apportée en r9289, et nouvelle correction du bug ...	notin	2006-10-31
*	Fix compile error	msozeau	2006-10-31
*	Work on obligation separation.	msozeau	2006-10-31
*	syntaxe du let in encore	barras	2006-10-31
*	assouplissement de la syntaxe du let de ltac: t1 ; let in autorise	barras	2006-10-31
*	Débranchement du polymorphisme de sorte sur les définitions dans Type	herbelin	2006-10-30
*	MAJ	herbelin	2006-10-30
*	typo	herbelin	2006-10-30
*	dependences	barras	2006-10-30
*	fixed field_simplify + changed precedence of let and fun in ltac	barras	2006-10-30