coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix bashism in doc generation.	glondu	2008-05-26
*	doc of coqchk + improved module cache and computation of module sets	barras	2008-05-23
*	Nouvelle doc pour les modules.	soubiran	2008-05-23
*	Strategy commands are now exported	barras	2008-05-22
*	refined the conversion oracle	barras	2008-05-21
*	MAJ crédits	herbelin	2008-05-19
*	- Fix bug related to indices of fixpoints.	msozeau	2008-05-13
*	MAJ et bricoles diverses	herbelin	2008-05-12
*	- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used to	msozeau	2008-05-12
*	- Cleanup parsing of binders, reducing to a single production for all	msozeau	2008-05-11
*	[ring] constructor for power was missing in the doc	barras	2008-05-06
*	Minor updates in the documentation of notations.	glondu	2008-05-05
*	Fix eauto still using delta when it shouldn't (should make CoRN compile	msozeau	2008-04-29
*	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
*	Correction bug 1838 + doc modules.	soubiran	2008-04-21
*	documentation tactique gappa	filliatr	2008-04-17
*	Add almost empty Classes.tex for documentation of type classes.	msozeau	2008-04-17
*	Document CHANGES in setoid rewrite, move DefaultRelation to	msozeau	2008-04-15
*	* added a subsection to explain the automatic declaration of schemes:	vsiles	2008-04-15
*	- Add "Global" modifier for instances inside sections with the usual	msozeau	2008-04-15
*	- Un peu de doc, préparation du CHANGES pour la release.	herbelin	2008-04-15
*	typo	vsiles	2008-04-15
*	Update doc and remove another overloading of equiv_*.	msozeau	2008-04-14
*	Bugs, nettoyage, et améliorations diverses	herbelin	2008-04-13
*	Document the new setoid rewrite tactic, and fix a few things while	msozeau	2008-04-12
*	Chgts mineurs:	herbelin	2008-04-03
*	Add option to set the opacity of obligations to transparent, to be able	msozeau	2008-04-01
*	Ajout d'abbréviations/notations paramétriques	herbelin	2008-03-30
*	Fix examples in Program documentation and add comindexes for the various	msozeau	2008-03-23
*	some references to IntMap forgotten in last commit	letouzey	2008-03-19
*	migration of the old IntMap library from StdLib to a user contrib (Cachan/Int...	letouzey	2008-03-19
*	Indexation de pose proof, et par la même occasion du nouveau specialize	herbelin	2008-03-10
*	f_equal, revert, specialize in ML, contradict in better Ltac (+doc)	letouzey	2008-03-07
*	repair for commit 10612 (due to grammar order, some syntaxes weren't working)	letouzey	2008-03-06
*	Rework on rich forms of rewrite	letouzey	2008-03-01
*	Bug dans la génération de la stdlib	notin	2008-02-27
*	Plongement de doc/Makefile dans la nouvelle architecutre des Makefile	notin	2008-02-14
*	Suppression de l'option -glob-from de Coqdoc: les globalisations sont	notin	2008-02-13
*	Fix the clrewrite tactic, change Relations.v to work on relations in Prop	msozeau	2008-02-09
*	Documentation of CHANGES and refman doc for the implicit argument binder	msozeau	2008-02-08
*	New "Preterm [ of id ] " command to show the preterm before giving it to	msozeau	2008-02-08
*	updates concerning FSets	letouzey	2008-02-08
*	- Documentation des nouvelles options d'implicites (Set Strongly Strict	herbelin	2008-02-06
*	Add new files theories/Program/Basics.v and theories/Classes/Relations.v	msozeau	2008-02-03
*	Unification de TacLetRecIn et TacLetIn. En particulier, on peut	herbelin	2008-02-01
*	Debug implementation of dependent induction/dependent destruction and documen...	msozeau	2008-01-31
*	Finish let\| implementation and document it	msozeau	2008-01-31
*	Added full documentation for mathematical mode (draft version)	corbinea	2008-01-29
*	Ajout d'une explication dans la FAQ pour le bug avec MOD4 sous Coqide	notin	2008-01-07