coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Using interp_genarg in tactic notations where possible, instead of an ad-hoc	Pierre-Marie Pédrot	2013-12-19
*	test-suite/output/Notations : evar number change	Pierre Boutillier	2013-12-19
*	Bad use of Obj.magic in interpretation of TacAlias arguments.	Pierre Boutillier	2013-12-19
*	Printing function for Stdargs in debugger	Pierre Boutillier	2013-12-19
*	Missing Fail in r16792	Pierre Boutillier	2013-12-19
*	test guard condition against feature incompatible with prop-ext	Bruno Barras	2013-12-17
*	Fix make install after 3e972b3ff8e532be233f70567c87512324c99b4e	Pierre Boutillier	2013-12-17
*	Merge branch 'trunk' of github.com:coq/coq into trunk	Matthieu Sozeau	2013-12-17
\|\
* \|	Tentative fix of the guardedness checker by Christine and me. All stdlib and ...	Matthieu Sozeau	2013-12-17
\| *	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot	2013-12-17
\|/
*	Get rid of messages "emitting ..." when compiling .v files	Pierre Letouzey	2013-12-16
*	A few fixes to the build system (mostly for ocamlbuild)	Pierre Letouzey	2013-12-16
*	Added test-suite for bug #2990.	Pierre-Marie Pédrot	2013-12-16
*	Dedicated inductive for return values of rewrite strategies.	Pierre-Marie Pédrot	2013-12-16
*	Do not overallocate closures' named environments in infos. Modifying the access	Pierre-Marie Pédrot	2013-12-15
*	Do not compile coqide with -thread	Pierre Boutillier	2013-12-12
*	Patch for supporting [From Xxx Require Yyy Zzz.]	Gregory Malecha	2013-12-12
*	Better unification for [projT1] and [proj1_sig].	Jason Gross	2013-12-12
*	Generalize eq_proofs_unicity	Jason Gross	2013-12-12
*	Documenting the tactic-in-term construction.	Pierre-Marie Pédrot	2013-12-11
*	Fix CoqIDE compilation under standard version of lablgtk2	Enrico Tassi	2013-12-11
*	Fixing backtrace registering of various tactic-related try-with blocks.	Pierre-Marie Pédrot	2013-12-11
*	Fix CoqIDE on windows	Enrico Tassi	2013-12-10
*	Renaming elisp files to avoid conflict with pg in distribs.	Pierre Courtieu	2013-12-10
*	Fix printing of Ltac's backtrace.	Arnaud Spiwack	2013-12-09
*	Stylistic change.	Arnaud Spiwack	2013-12-09
*	Fix test-suite/success/evars.v.	Arnaud Spiwack	2013-12-06
*	Remove duplicate test-suite file.	Arnaud Spiwack	2013-12-06
*	Fix the refine related test-suite files to account for the new refine.	Arnaud Spiwack	2013-12-06
*	Missing file in commit 1fb883.	Arnaud Spiwack	2013-12-06
*	Fix g_derive.ml4.	Arnaud Spiwack	2013-12-04
*	Documentation of the Derive plugin.	Arnaud Spiwack	2013-12-04
*	Stm: remove an assertion.	Arnaud Spiwack	2013-12-04
*	Derive plugin.	Arnaud Spiwack	2013-12-04
*	Fix Admitted.	Arnaud Spiwack	2013-12-04
*	Proof_global: fix start_proof comment after the preceding commits.	Arnaud Spiwack	2013-12-04
*	Factoring(continued).	Arnaud Spiwack	2013-12-04
*	Refactoring: storing more information in the terminator closure.	Arnaud Spiwack	2013-12-04
*	The commands that initiate proofs are now in charge of what happens when proo...	Arnaud Spiwack	2013-12-04
*	Vernac classification: allow for commands which start proofs but must be sync...	Arnaud Spiwack	2013-12-04
*	Allow proofs to start with dependent goals.	Arnaud Spiwack	2013-12-04
*	Improved the presentation of the proof of UIP_refl_nat.	Hugo Herbelin	2013-12-04
*	Add lemma derivable_pt_lim_atan.	Guillaume Melquiond	2013-12-04
*	Removing useless meta-related functions.	Pierre-Marie Pédrot	2013-12-03
*	Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.	Guillaume Melquiond	2013-12-03
*	Silence some warning about references in documentation.	Guillaume Melquiond	2013-12-03
*	Remove a useless hypothesis from Rle_Rinv.	Guillaume Melquiond	2013-12-03
*	Ensure locality modifiers are properly highlighted in CoqIDE.	Guillaume Melquiond	2013-12-03
*	Silence compilation warning by avoiding some deprecated constructs.	Guillaume Melquiond	2013-12-03
*	Test case for bug#2848.	xclerc	2013-12-02