coq - The formal proof system

Age	Commit message (Expand)	Author
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-03	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-02	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-01	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-11-30	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-29	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-28	Testsuite: remove the logic for 'bugs/opened/shouldnotsucceed' (unused)	xclerc
2013-11-27	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-26	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-25	Remove the Hiddentac module.	Arnaud Spiwack
2013-11-25	Factoring: is_section_variable.	Arnaud Spiwack