coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Correction du bug #2214 + maj liens web	notin	2010-02-26
*	mingw32 cross-compilation: coqide.exe as a GUI program, nicer ./build script	letouzey	2010-02-25
*	ide/coq_lex.ml in .gitignore	letouzey	2010-02-25
*	Enabled natdynlink hack on Mac OS 10.6	thutchin	2010-02-25
*	In the git-specific part of Makefile.build, call to hostname gave option	thutchin	2010-02-25
*	Various fixes in interp, session switching and backtracking	vgross	2010-02-25
*	Changes in lexing and tagging.	vgross	2010-02-25
*	Ignoring .spit/.spot files from OCamlSpotter	thutchin	2010-02-25
*	Win32 cross-compilation from debian: build of coqide.exe and other binaries	letouzey	2010-02-24
*	correction of bug #2088	jforest	2010-02-24
*	Improve unification when evars and metas are mixed.	msozeau	2010-02-22
*	added validation of delta_resolver (which seem to have an impact on typing)	barras	2010-02-19
*	[checker] fixed vo validation problems, module incompatibilities remain	barras	2010-02-19
*	Fixing compilation issues	vgross	2010-02-19
*	Removed redundant and ill-named technical lemma.	gmelquio	2010-02-18
*	Removed SeqProp's dependency on Classical.	gmelquio	2010-02-18
*	Removed Rtrigo's dependency on Classical.	gmelquio	2010-02-18
*	Fixing modules names.	vgross	2010-02-18
*	Experimental build of coqtop.exe + plugins via cross-compilation linux-->win32	letouzey	2010-02-18
*	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