coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	CThread: use a different type for thread friendly in_channels	Enrico Tassi	2014-12-17
*	Summary: more surgery functions	Enrico Tassi	2014-12-17
*	Global: export the name of the summary entry	Enrico Tassi	2014-12-17
*	Dyn: add API to check of two Dyn.t are ==	Enrico Tassi	2014-12-17
*	Arguments: warn only if no option is given (Close 3860)	Enrico Tassi	2014-12-17
*	CoqIDE: better messages	Enrico Tassi	2014-12-17
*	Revert and correctly fix "#4843 part 2 : The .cmxs files for plugins must hav...	Pierre Boutillier	2014-12-17
*	#3828 is solved.	Hugo Herbelin	2014-12-16
*	Moving #2447 (congruence) to fixed.	Hugo Herbelin	2014-12-16
*	In CHANGES, alerting about stronger check on notation level modifiers.	Hugo Herbelin	2014-12-16
*	More printers for ltac signatures.	Hugo Herbelin	2014-12-16
*	Test for #3654.	Hugo Herbelin	2014-12-16
*	fix bug #2447 in congruence	Pierre Corbineau	2014-12-16
\|\
* \|	fix bug #2447 in congruence	Pierre Corbineau	2014-12-16
\| *	Fixing CAMLP4 compilation.	Pierre-Marie Pédrot	2014-12-16
\| *	msg_info now puts infomsg tag in emacs mode.	Pierre Courtieu	2014-12-16
\| *	Proper thread-safe implementation for Exninfo.	Pierre-Marie Pédrot	2014-12-16
\| *	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
\| *	Error messages of Searchxxx are coherent with goal selector.	Pierre Courtieu	2014-12-16
\|/
*	Fix for #3154: use CUnix.sys_command to call native compiler.	Maxime Dénès	2014-12-16
*	Changed bullet informations to warning for better display in PG.	Pierre Courtieu	2014-12-15
*	Adapted test file for About.	Pierre Courtieu	2014-12-15
*	Tentatively starting to use heuristics for evar-evar resolution: first	Hugo Herbelin	2014-12-15
*	Failing on unbound notation variable in notation level modifiers	Hugo Herbelin	2014-12-15
*	New try on Fixing an evar_map bug revealed by commit 603b66f81 on	Hugo Herbelin	2014-12-15
*	Tests for #3848 and #3854.	Hugo Herbelin	2014-12-15
*	Documenting check_record + changing a possibly undefined int into int option.	Hugo Herbelin	2014-12-15
*	About now accepts hypothesis names and goal selector.	Pierre Courtieu	2014-12-15
*	Fix treatment of universe context in typecheck inductive (was added	Matthieu Sozeau	2014-12-15
*	Tests for Searchxxx commands added and modified.	Pierre Courtieu	2014-12-15
*	Fixing bug #3865.	Pierre-Marie Pédrot	2014-12-15
*	Util.un_op -> Option.default	Pierre Boutillier	2014-12-14
*	Fix merging of name maps in union of universe contexts.	Matthieu Sozeau	2014-12-14
*	Fixing bug #3858 and #3817 in one stroke.	Pierre-Marie Pédrot	2014-12-14
*	Revert "Fixing bug #3817."	Pierre-Marie Pédrot	2014-12-14
*	Add Ltac syntax for the [tclIFCATCH] primitive.	Arnaud Spiwack	2014-12-12
*	Make sure the goals on the shelve are identified as goal and unresolvable for...	Arnaud Spiwack	2014-12-12
*	Searchxxx now interpret patterns in goal environment if any.	Pierre Courtieu	2014-12-12
*	#4843 part 2 : The .cmxs files for plug-ins must have execute permission	Pierre Boutillier	2014-12-12
*	Fix #3163 and #3843 part 1 : Cygwin DLLs have extension ".so", not ".dll"	Pierre Boutillier	2014-12-12
*	Fix #3800 : cmxs need execution priviledges under windows	Pierre Boutillier	2014-12-12
*	An option SimplIsCbn	Pierre Boutillier	2014-12-12
*	Extend the syntax of simpl with a delta flag.	Arnaud Spiwack	2014-12-12
*	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu	2014-12-12
*	Two fixes in unification (bugs #3782 and #3709)	Matthieu Sozeau	2014-12-12
*	In discrimination nets, do not index lambdas if they're part of a beta	Matthieu Sozeau	2014-12-12
*	handling Functional Scheme for required but not imported modules	Julien Forest	2014-12-11
*	List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)	Pierre Letouzey	2014-12-11
*	First series of results on lists.	Sébastien Hinderer	2014-12-11
*	Commit not ready. Sorry.	Hugo Herbelin	2014-12-11