coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Min, Max: for avoiding inelegant NPeano.max printing, we Export this lib	letouzey	2010-02-10
*	bugs/.../1784.v: revert Matthieu's recent fix, since Program has been made co...	letouzey	2010-02-10
*	Euclidean division for NArith	letouzey	2010-02-10
*	splitted -> split	glondu	2010-02-10
*	Fix [Existing Class] impl and add documentation. Fix computation of the	msozeau	2010-02-10
*	Numbers: properties of min/max with respect to 0,S,P,add,sub,mul	letouzey	2010-02-09
*	NPeano improved, subsumes NatOrderedType	letouzey	2010-02-09
*	NSub: a missing lemma (sub usually decreases)	letouzey	2010-02-09
*	NBinary improved, contains more, subsumes NOrderedType	letouzey	2010-02-09
*	ZBinary (impl of Numbers via Z) reworked, comes earlier, subsumes ZOrderedType	letouzey	2010-02-09
*	DoubleCyclic + NMake : typeclasses, more genericity, less ML macro-generation	letouzey	2010-02-08
*	Added a lazy evaluation of the composition of module substitutions. It improv...	soubiran	2010-02-04
*	fix commit 12706 + comments.	soubiran	2010-02-03
*	Small fix on module inclusion.	soubiran	2010-02-02
*	Update CHANGES, add documentation for new commands/tactics and do a bit	msozeau	2010-01-30
*	Division in numbers: kills some Include to avoid bad alias Zsucc = ZDiv.Z.Z'.S	letouzey	2010-01-29
*	minor change in test-suite/output/NumberSyntax.out: a BigN.t_ instead of BigN.t	letouzey	2010-01-29
*	Remove bashisms	glondu	2010-01-28
*	New command Declare Reduction <id> := <conv_expr>.	letouzey	2010-01-28
*	Fix previous commit	notin	2010-01-28
*	Fix implicit_application for let-bound variables in the class context.	msozeau	2010-01-28
*	Typo in previous commit	notin	2010-01-28
*	Correction du bug #2219: application du patch envoyé par F. Garillot	notin	2010-01-28
*	Backport fixes in Instance declarations to Program Instance.	msozeau	2010-01-28
*	Support for generalized rewriting under dependent binders, using the	msozeau	2010-01-26
*	Quick fix for references to section variables unbound in the current	msozeau	2010-01-26
*	Add [Next Obligation with tactic] support (wish #1953).	msozeau	2010-01-26
*	make init + NMake.v/NMake_gen.v	notin	2010-01-26
*	Add -makecmd configure option	glondu	2010-01-26
*	NMake (and hence BigN): shiftr, shiftl now in the signature NSig	letouzey	2010-01-25
*	NMake: several things need not be macro-generated	letouzey	2010-01-25
*	Ring31 : a ring structure and tactic for int31	letouzey	2010-01-19
*	NMake_gen: fix previous commit (some spaces were critical), remove some more ...	letouzey	2010-01-19
*	NMake_gen: no more spaces at end of lines	letouzey	2010-01-19
*	Various bug fix on recent features of the module system:	soubiran	2010-01-19
*	More improvements of BigN, BigZ, BigQ:	letouzey	2010-01-18
*	BigN, BigZ, BigQ: presentation via unique module with both ops and props	letouzey	2010-01-17
*	Simplification of OrdersTac thanks to the functor application ! with no inline	letouzey	2010-01-17
*	Variant !F M for functor application that does not honor the Inline declarations	letouzey	2010-01-17
*	Report de la révision #12676	notin	2010-01-15
*	Fix uncaught exception	vgross	2010-01-14
*	Document Local Declare ML Module	glondu	2010-01-14
*	Avoid some more re-declarations of Equivalence instances	letouzey	2010-01-14
*	Rename Zbinary into Zdigit in order to avoid confusion with Numbers/.../ZBina...	letouzey	2010-01-14
*	Fix bug #2086, error message when we match on an non-inductive type.	msozeau	2010-01-14
*	- Show Obligation Tactic	msozeau	2010-01-14
*	Add *.annot to .gitignore	glondu	2010-01-14
*	Disable validate	glondu	2010-01-14
*	Try to avoid re-declaring Equivalence, especially for Logic.eq	letouzey	2010-01-13
*	GenericMinMax: still a min_case_strong with hypothesis in the wrong order	letouzey	2010-01-12