coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Micromega: doc + test-suite update	fbesson	2008-07-07
*	Improved robustness of micromega parser. Proof search of Micromega test-suite...	fbesson	2008-07-02
*	Documentation Prop<=Set et Arguments Scope Global	herbelin	2008-07-01
*	correction sur la doc des modules	soubiran	2008-07-01
*	Lissage de la gestion des chemins de chargement de fichiers :	herbelin	2008-06-29
*	Micromega : bugs fixes - renaming of tactics - documentation	fbesson	2008-06-25
*	Typo in documentation (isn't it?)	glondu	2008-06-25
*	Les contraintes d'univers sont maintenant collectées dans le champs mod_cons...	soubiran	2008-06-25
*	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
*	Numéros de version dans la doc	notin	2008-06-13
*	- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)	herbelin	2008-06-10
*	2-3 petites modifs sur la doc	notin	2008-06-10
*	Fix a typo	glondu	2008-06-09
*	Documentation de "instantiate".	glondu	2008-06-09
*	- Documentation de admit et Print Assumptions.	herbelin	2008-06-09
*	- Extension de "generalize" en "generalize c as id at occs".	herbelin	2008-06-08
*	Second pass on typeclasses documentation, fix html rendering.	msozeau	2008-06-08
*	Fix library index template and associated script.	msozeau	2008-06-07
*	Fix setoid_rewrite documentation examples.	msozeau	2008-06-03
*	Intropattern: syntax {x,y,z,t} becomes (x & y & z & t), as decided in	letouzey	2008-06-01
*	remove additional occurrences of +/- forgotten in commit 11030	letouzey	2008-06-01
*	Bactrack sur +, - dans rewrite qui, redondants avec ->, <-, n'en sont qu'à	herbelin	2008-06-01
*	Notation concise pour la valeur par défaut des cas reconnus comme	herbelin	2008-05-28
*	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