coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	Porting type interpretation in Tacinterp to the new tactics.	Pierre-Marie Pédrot	2013-12-02
*	Writing [cut] tactic using the new monad.	Pierre-Marie Pédrot	2013-12-02
*	Test suite: update output reference.	xclerc	2013-12-02
*	Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr//gitroot/coq/coq into t...	xclerc	2013-12-02
\|\
* \|	Print logical name rather than path (thus allowing reproducible tests).	xclerc	2013-12-02
\| *	Removing RefArgType generic argument.	Pierre-Marie Pédrot	2013-12-01
\| *	Ensuring the right parsing of glob arguments, used by refine	Pierre-Marie Pédrot	2013-12-01
\| *	Fixing ltac constr variable handling in refine.	Pierre-Marie Pédrot	2013-11-30
\| *	Adding printing of ltac envs to debugger.	Pierre-Marie Pédrot	2013-11-30
\| *	Getting rid of casted_open_constr. It was only used by the	Pierre-Marie Pédrot	2013-11-30
\| *	Better heuristic for name generation backward compatibility. We fallback	Pierre-Marie Pédrot	2013-11-30
\| *	Useless instantiation function exported in Evd.	Pierre-Marie Pédrot	2013-11-30
\| *	Tentative fix to recover fresh name generation as it was before	Pierre-Marie Pédrot	2013-11-30
\| *	First stab at documenting Canonical Structures	Enrico Tassi	2013-11-29
\| *	Fixing bug #3169 and avoiding anomaly in bug #2885 (vm_compute not	Hugo Herbelin	2013-11-29
\|/
*	Testsuite: flatten the 'bugs/opened' directory.	xclerc	2013-11-29
*	Testsuite: remove the logic for 'bugs/opened/shouldnotsucceed' (unused)	xclerc	2013-11-28
*	Getting rid of goal-dependency in declarative mode argument evaluation.	Pierre-Marie Pédrot	2013-11-27
*	Fixing abstract tactic by using a dummy name out of a declared proof.	Pierre-Marie Pédrot	2013-11-27
*	Actually adding the grammar entry to handle tactics in terms.	Pierre-Marie Pédrot	2013-11-27
*	Adding the necessary hooks to handle tactics in terms.	Pierre-Marie Pédrot	2013-11-27
*	Adding generic solvers to term holes. For now, no resolution mechanism nor	Pierre-Marie Pédrot	2013-11-27
*	Old message Interp returns the state id so that one can BackTo it	Enrico Tassi	2013-11-27
*	New option --help-XML-protocol to document the XML procol used by -ideslave	Enrico Tassi	2013-11-27
*	First stab at retrocompatible INTERP message	Enrico Tassi	2013-11-27
*	Use my real email address in .mailmap	Enrico Tassi	2013-11-27
*	Reduction: every n iterations a slaves process checks for interruption	Enrico Tassi	2013-11-27
*	STM: restart slave after every proof	Enrico Tassi	2013-11-27
*	CoqIDE: show error message for parsing errors	Enrico Tassi	2013-11-27
*	Adding a generic Int.Map using persistent arrays.	Pierre-Marie Pédrot	2013-11-26
*	Do not use ugly Dyn features in the Quote plugin. Use instead the	Pierre-Marie Pédrot	2013-11-26
*	Remove the Hiddentac module.	Arnaud Spiwack	2013-11-25
*	Factoring: is_section_variable.	Arnaud Spiwack	2013-11-25
*	Tacinterp: fewer use of old-style goals.	Arnaud Spiwack	2013-11-25
*	Typo resulting in bad eta-expansion of destructing let's body.	Hugo Herbelin	2013-11-25
*	Better implementation of summary unfreezing.	Pierre-Marie Pédrot	2013-11-24