coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Add enough information to correctly globalize recursive calls in inductive and	msozeau	2008-09-11
*	Update CHANGES and INSTALL	glondu	2008-09-07
*	Renaming parser -> coq-parser	glondu	2008-08-18
*	Évolutions diverses et variées.	herbelin	2008-08-04
*	Add -browser option to configure script	glondu	2008-07-27
*	Fixed doc of inductive sort-polymorphism (cf bug #1908). Seized the	herbelin	2008-07-23
*	- Suppression de Rstar/Newman peu utilisables comme biblio (encodage	herbelin	2008-07-17
*	Quelques modifications autour du filtrage Ltac:	herbelin	2008-07-16
*	Documentation Prop<=Set et Arguments Scope Global	herbelin	2008-07-01
*	Lissage de la gestion des chemins de chargement de fichiers :	herbelin	2008-06-29
*	MAJ fichiers spécifiques trunk	herbelin	2008-06-22
*	Rename obligations_tactic to obligation_tactic and fix bugs #1893.	msozeau	2008-06-22
*	- Implantation de la suggestion 1873 sur discriminate. Au final,	herbelin	2008-06-21
*	MAJ diverses	herbelin	2008-06-11
*	Documentation de "instantiate".	glondu	2008-06-09
*	- Documentation de admit et Print Assumptions.	herbelin	2008-06-09
*	- Patch sur "intros until 0"	herbelin	2008-06-08
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	add tiny change to coqide	jnarboux	2008-06-07
*	One (last?) more update of CHANGES.	letouzey	2008-06-05
*	more updates of CHANGES	letouzey	2008-06-04
*	Some updates of CHANGES (to be continued...)	letouzey	2008-06-03
*	Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in	letouzey	2008-06-01
*	- Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"	herbelin	2008-05-30
*	update changes related to coqide	jnarboux	2008-05-27
*	- Nouvelle option "Set Printing Existential Instances" pour forcer	herbelin	2008-05-25
*	Ajout de la possibilité d'utiliser fix/cofix dans les notations.	herbelin	2008-05-24
*	refined the conversion oracle	barras	2008-05-21
*	Léger backtrack sur commit coqide précédent (si la commande à annuler	herbelin	2008-05-20
*	- Fix bug related to indices of fixpoints.	msozeau	2008-05-13
*	MAJ et bricoles diverses	herbelin	2008-05-12
*	- Cleanup parsing of binders, reducing to a single production for all	msozeau	2008-05-11
*	Backtrack sur la mise à disposition en standard de la notation [ x ; ... ; y ]	herbelin	2008-05-09
*	Mise en place d'un algorithme d'inversion des contraintes de type lors	herbelin	2008-05-05
*	Réutilisation de l'infrastructure pour le polymorphisme d'univers des	herbelin	2008-04-30
*	Ajout notation [ x ; ... ; y ] dans list_scope. Changement de la	herbelin	2008-04-29
*	- Backtrack sur option with_types suite à confusion sur l'utilisation	herbelin	2008-04-27
*	- Backtrack sur extension de syntaxe pour pose qui rentre en conflit avec	herbelin	2008-04-26
*	Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour	herbelin	2008-04-26
*	Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuve	herbelin	2008-04-25
*	Change default eauto depth to 100 in setoid_rewrite, bump necessary	msozeau	2008-04-23
*	Bug squashing day !	msozeau	2008-04-17
*	Mises à jour bugs, CHANGES, code mort	herbelin	2008-04-15
*	Document CHANGES in setoid rewrite, move DefaultRelation to	msozeau	2008-04-15
*	- Un peu de doc, préparation du CHANGES pour la release.	herbelin	2008-04-15
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Suite 10760	herbelin	2008-04-05
*	Mise en place d'une extension de apply pour que celui-ci sache	herbelin	2008-04-04
*	Quelques améliorations des intro patterns:	herbelin	2008-04-04
*	Ajout "simple apply" et "simple eapply" pour apply sans unfold	herbelin	2008-04-01