coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	Adding uim files	vgross	2010-02-18
*	Polishing the setup of CoqIDE Input Method	vgross	2010-02-18
*	Removed Rseries' dependency on Classical.	gmelquio	2010-02-17
*	RelationClasses: adapt eq_Reflexive and co to avoid Universe Inconsistencies	letouzey	2010-02-17
*	Kill some useless dependencies (Bvector, Program.Syntax)	letouzey	2010-02-17
*	Arith's min and max placed in Peano (+basic specs max_l and co)	letouzey	2010-02-17
*	Removed Rlimit's dependency on Classical.	gmelquio	2010-02-17
*	Removed Rderiv's dependency on Classical.	gmelquio	2010-02-17
*	Compute the correct generalization information when discharging a class	msozeau	2010-02-16
*	Fix sort_dependencies for good, maintaining the initial order.	msozeau	2010-02-16
*	Makefile.build: avoid warning about undefined variable during make install	letouzey	2010-02-16
*	Makefile: also install the .cmi of plugins	letouzey	2010-02-16
*	Uniformisation Sorting/Mergesort and Structures/Orders	letouzey	2010-02-16
*	Change the customization of modifiers (bug #2210)	vgross	2010-02-15
*	Util.lowercase_unicode: avoid creating the segmenttree each time (speeds some...	letouzey	2010-02-15
*	update CHANGES : ocamlbuild, Structures, Numbers, MSets ... (cf. commit 8.3 r...	letouzey	2010-02-14
*	CompSpec2Type is used to build functions, it should be Defined, not Qed	letouzey	2010-02-13
*	Fix NumbersSyntax.out	letouzey	2010-02-13
*	Mycamlbuild: change name of autogenerated file : NMake -> Nmake_gen	letouzey	2010-02-12
*	Simplify backtracking	vgross	2010-02-12
*	Fixing closing of segments.	vgross	2010-02-12
*	Delineating a API for Coq inside toplevel/vernac.ml	vgross	2010-02-12
*	Refactoring of the printing options	vgross	2010-02-12
*	CompSpecType, a clone of CompSpec but in Type instead of Prop	letouzey	2010-02-12
*	Remove LocallySorted.v added by mistake at the root of the archive	letouzey	2010-02-12
*	Cleanup in Classes, removing unsupported code.	msozeau	2010-02-11
*	Documentation of the ! annotation for functor application	letouzey	2010-02-11
*	ajout test de fied_simplify_eq in	barras	2010-02-10
*	bug in field_simplify_eq in	barras	2010-02-10
*	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