coq - The formal proof system

Age	Commit message (Expand)	Author
2013-12-17	Removing the need of evarmaps in constr internalization.	Pierre-Marie Pédrot
2013-12-16	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-15	Do not overallocate closures' named environments in infos. Modifying the access	Pierre-Marie Pédrot
2013-12-12	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-11	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-10	Fix CoqIDE on windows	Enrico Tassi
2013-12-10	Renaming elisp files to avoid conflict with pg in distribs.	Pierre Courtieu
2013-12-09	Fix printing of Ltac's backtrace.	Arnaud Spiwack
2013-12-09	Stylistic change.	Arnaud Spiwack
2013-12-06	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-04	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-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