coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Tactic extensions do not need to be classified by the STM, as	Pierre-Marie Pédrot	2014-02-05
*	The constructor tactic now returns several successes.	Pierre-Marie Pédrot	2014-02-04
*	Tracking memory misallocation by trying to improve sharing.	Pierre-Marie Pédrot	2014-02-03
*	Allocation-friendly mapping functions in Nametab.	Pierre-Marie Pédrot	2014-02-03
*	Allocation friendly map-handling functions in Dag.	Pierre-Marie Pédrot	2014-02-03
*	Fixing backtrace reporting.	Pierre-Marie Pédrot	2014-02-02
*	Fixing bug #3226.	Pierre-Marie Pédrot	2014-02-02
*	Removing the [Require "file"] syntax.	Pierre-Marie Pédrot	2014-02-02
*	In Ltac's exact tactic: avoid checking the type of the term twice.	Arnaud Spiwack	2014-01-31
*	Typos in comment.	Arnaud Spiwack	2014-01-31
*	Coqmktop without Sys.command, changes in ./configure -*byteflags options	Pierre Letouzey	2014-01-30
*	Relaunch all Unix.waitpid when they ended with EINTR	Pierre Letouzey	2014-01-30
*	CUnix: enriched (get_extension, sys_command, waitpid_non_intr) + cleaned	Pierre Letouzey	2014-01-30
*	Mltop: explicitly qualify calls to CUnix	Pierre Letouzey	2014-01-30
*	CString: avoid redefining is_sub	Pierre Letouzey	2014-01-30
*	Remove useless Xml_utils	Pierre Letouzey	2014-01-30
*	Get rid of two utility files, obsolete now that configure is a .ml	Pierre Letouzey	2014-01-30
*	clib.mllib: remove duplicated Flags entry	Pierre Letouzey	2014-01-30
*	G_xml: remove some duplication in error fonctions	Pierre Letouzey	2014-01-30
*	G_xml: protect against some possible Not_found	Pierre Letouzey	2014-01-30
*	Load implemented in CoqIDE/STM (closes: #3223)	Enrico Tassi	2014-01-30
*	STM + CoqIDE: stop_worker message and UI	Enrico Tassi	2014-01-30
*	Work around for bug in threads + blocking io streamlined	Enrico Tassi	2014-01-30
*	STM: worker sends back to master the last valid state	Enrico Tassi	2014-01-30
*	STM: tell the user if the master is recomputing states validated by workers	Enrico Tassi	2014-01-30
*	Fixing backtrace handling here and there.	Pierre-Marie Pédrot	2014-01-30
*	Using Map.smartmap whenever deemed useful.	Pierre-Marie Pédrot	2014-01-29
*	Adding a smartmap[i] operator to maps.	Pierre-Marie Pédrot	2014-01-29
*	Fixing dependent inversion. Some exceptions were not caught by the tactic	Pierre-Marie Pédrot	2014-01-28
*	Abstracting away coercion indexes in Classops.	Pierre-Marie Pédrot	2014-01-27
*	Coercions: avoid imperative data structure	Enrico Tassi	2014-01-26
*	-schedule-vi-checking ported to spawn	Enrico Tassi	2014-01-26
*	CoqIDE: command line for extra coqtop "flags"	Enrico Tassi	2014-01-26
*	break > 80 cols line	Enrico Tassi	2014-01-26
*	STM: ported to spawn	Enrico Tassi	2014-01-26
*	CoqIDE: ported to spawn	Enrico Tassi	2014-01-26
*	Spawn: managed processes	Enrico Tassi	2014-01-26
*	configure.ml fixed wrt Win32 + byte-only + coqide	Enrico Tassi	2014-01-26
*	Adding a test for bug #3023.	Pierre-Marie Pédrot	2014-01-25
*	More in CHANGES.	Pierre-Marie Pédrot	2014-01-25
*	[Coercion]s use [Sortclass], not [Prop] (in docs)	Jason Gross	2014-01-24
*	The configure script now outputs the parameters it was fed with in	Pierre-Marie Pédrot	2014-01-24
*	bug correction in proving principles of function	jforest	2014-01-20
*	Using full paths in coqdep -dumpgraph.	Pierre-Marie Pédrot	2014-01-19
*	Fixing coqdep graph printing. The transitive reduction algorithm was bugged.	Pierre-Marie Pédrot	2014-01-19
*	Adding a default object to generic argument registering mechanism.	Pierre-Marie Pédrot	2014-01-19
*	Fixing an interpretation bug with tactics in notations. For some obscure	Pierre-Marie Pédrot	2014-01-19
*	Fixing checker compilation, which was broken by the following commit:	Pierre-Marie Pédrot	2014-01-19
*	Relaxing the sort elimination check to allow for let-bindings in arities.	Maxime Dénès	2014-01-18
*	Makefiles use $(foo), not $foo, for variables	Jason Gross	2014-01-18