coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	STM: simple refactoring	Enrico Tassi	2014-01-04
*	Future: allow custom action when a delegated future is forced	Enrico Tassi	2014-01-04
*	kernel: save in aux the list of section variables used	Enrico Tassi	2014-01-04
*	STM: set loc for aux file when interpreting vernac	Enrico Tassi	2014-01-04
*	STM: record in aux file proof build and check time	Enrico Tassi	2014-01-04
*	Aux_file: cache information at compile time for later (re)use	Enrico Tassi	2014-01-04
*	Remove obsolete comment about Let being processed synchronously	Enrico Tassi	2014-01-04
*	Code cleaning in Rewrite, may also result faster.	Pierre-Marie Pédrot	2014-01-04
*	Reference the 'external' tactic.	Guillaume Melquiond	2014-01-01
*	When resetting an evarmap with the unsafe function Evd.evars_reset_evd with	Pierre-Marie Pédrot	2013-12-30
*	Useless Evd.create_evar_defs.	Pierre-Marie Pédrot	2013-12-30
*	Support for evars and metas in native compiler.	Maxime Dénès	2013-12-30
*	Avoid generating .ml files in native compiler.	Maxime Dénès	2013-12-29
*	Got rid of unused lazy flag in the native compiler.	Maxime Dénès	2013-12-29
*	Revert "Partial revert of r16711"	Maxime Dénès	2013-12-28
*	Removing native_name reference from constant_body.	Maxime Dénès	2013-12-28
*	STM: capture type checking error (Closes: 3195)	Enrico Tassi	2013-12-24
*	Qed: feedback when type checking is done	Enrico Tassi	2013-12-24
*	CoqIDE: new feedback "incomplete" to signal partial Qed	Enrico Tassi	2013-12-24
*	Future: optional greedy chaining	Enrico Tassi	2013-12-24
*	cleanup warning	Enrico Tassi	2013-12-24
*	Simplifying the use of hypinfos in Rewrite.	Pierre-Marie Pédrot	2013-12-24
*	Rewrite.ml: removing direction flag from hypinfo.	Pierre-Marie Pédrot	2013-12-23
*	Do not pass unification flags around in Rewrite.	Pierre-Marie Pédrot	2013-12-22
*	Slight code cleaning ensuring more static invariants in Rewrite.	Pierre-Marie Pédrot	2013-12-22
*	Adding -bt to coqc.	Pierre-Marie Pédrot	2013-12-22
*	Adding a finer-grained -bt flag to coqtop only triggering backtraces.	Pierre-Marie Pédrot	2013-12-22
*	Notation variables are now taken into account as possible ltac bound variables	Pierre-Marie Pédrot	2013-12-22
*	Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at	Pierre-Marie Pédrot	2013-12-22
*	Notations can now accept dummy arguments. If ever a bound variable is not	Pierre-Marie Pédrot	2013-12-22
*	Test case for the buggy commutative cut subterm rule.	Maxime Dénès	2013-12-21
*	configure.ml: our configure script is now written in ML :-)	Pierre Letouzey	2013-12-20
*	Makefile.build: avoid a -pp	Pierre Letouzey	2013-12-20
*	coqc: execvp is now available even on win32	Pierre Letouzey	2013-12-20
*	coqmktop without Unix (simpler all_subdirs)	Pierre Letouzey	2013-12-20
*	Remove unused Makefile lines about .elc compilation	Pierre Letouzey	2013-12-20
*	Warning removal	Pierre Boutillier	2013-12-20
*	List: Bug 3039 weaker requirement for fold symmetric	Pierre Boutillier	2013-12-20
*	Coqdep always uses / as dir_sep	Pierre Boutillier	2013-12-20
*	micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...	Frédéric Besson	2013-12-20
*	Removing the useless pattern ident genarg.	Pierre-Marie Pédrot	2013-12-19
*	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