aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Get rid of messages "emitting ..." when compiling .v filesGravatar Pierre Letouzey2013-12-16
* A few fixes to the build system (mostly for ocamlbuild)Gravatar Pierre Letouzey2013-12-16
* Added test-suite for bug #2990.Gravatar Pierre-Marie Pédrot2013-12-16
* Dedicated inductive for return values of rewrite strategies.Gravatar Pierre-Marie Pédrot2013-12-16
* Do not overallocate closures' named environments in infos. Modifying the accessGravatar Pierre-Marie Pédrot2013-12-15
* Do not compile coqide with -threadGravatar Pierre Boutillier2013-12-12
* Patch for supporting [From Xxx Require Yyy Zzz.]Gravatar Gregory Malecha2013-12-12
* Better unification for [projT1] and [proj1_sig].Gravatar Jason Gross2013-12-12
* Generalize eq_proofs_unicityGravatar Jason Gross2013-12-12
* Documenting the tactic-in-term construction.Gravatar Pierre-Marie Pédrot2013-12-11
* Fix CoqIDE compilation under standard version of lablgtk2Gravatar Enrico Tassi2013-12-11
* Fixing backtrace registering of various tactic-related try-with blocks.Gravatar Pierre-Marie Pédrot2013-12-11
* Fix CoqIDE on windowsGravatar Enrico Tassi2013-12-10
* Renaming elisp files to avoid conflict with pg in distribs.Gravatar Pierre Courtieu2013-12-10
* Fix printing of Ltac's backtrace.Gravatar Arnaud Spiwack2013-12-09
* Stylistic change.Gravatar Arnaud Spiwack2013-12-09
* Fix test-suite/success/evars.v.Gravatar Arnaud Spiwack2013-12-06
* Remove duplicate test-suite file.Gravatar Arnaud Spiwack2013-12-06
* Fix the refine related test-suite files to account for the new refine.Gravatar Arnaud Spiwack2013-12-06
* Missing file in commit 1fb883.Gravatar Arnaud Spiwack2013-12-06
* Fix g_derive.ml4.Gravatar Arnaud Spiwack2013-12-04
* Documentation of the Derive plugin.Gravatar Arnaud Spiwack2013-12-04
* Stm: remove an assertion.Gravatar Arnaud Spiwack2013-12-04
* Derive plugin.Gravatar Arnaud Spiwack2013-12-04
* Fix Admitted.Gravatar Arnaud Spiwack2013-12-04
* Proof_global: fix start_proof comment after the preceding commits.Gravatar Arnaud Spiwack2013-12-04
* Factoring(continued).Gravatar Arnaud Spiwack2013-12-04
* Refactoring: storing more information in the terminator closure.Gravatar Arnaud Spiwack2013-12-04
* The commands that initiate proofs are now in charge of what happens when proo...Gravatar Arnaud Spiwack2013-12-04
* Vernac classification: allow for commands which start proofs but must be sync...Gravatar Arnaud Spiwack2013-12-04
* Allow proofs to start with dependent goals.Gravatar Arnaud Spiwack2013-12-04
* Improved the presentation of the proof of UIP_refl_nat.Gravatar Hugo Herbelin2013-12-04
* Add lemma derivable_pt_lim_atan.Gravatar Guillaume Melquiond2013-12-04
* Removing useless meta-related functions.Gravatar Pierre-Marie Pédrot2013-12-03
* Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Gravatar Guillaume Melquiond2013-12-03
* Silence some warning about references in documentation.Gravatar Guillaume Melquiond2013-12-03
* Remove a useless hypothesis from Rle_Rinv.Gravatar Guillaume Melquiond2013-12-03
* Ensure locality modifiers are properly highlighted in CoqIDE.Gravatar Guillaume Melquiond2013-12-03
* Silence compilation warning by avoiding some deprecated constructs.Gravatar Guillaume Melquiond2013-12-03
* Test case for bug#2848.Gravatar xclerc2013-12-02
* Porting type interpretation in Tacinterp to the new tactics.Gravatar Pierre-Marie Pédrot2013-12-02
* Writing [cut] tactic using the new monad.Gravatar Pierre-Marie Pédrot2013-12-02
* Test suite: update output reference.Gravatar xclerc2013-12-02
* Merge branch 'trunk' of git+ssh://scm.gforge.inria.fr//gitroot/coq/coq into t...Gravatar xclerc2013-12-02
|\
* | Print logical name rather than path (thus allowing reproducible tests).Gravatar xclerc2013-12-02
| * Removing RefArgType generic argument.Gravatar Pierre-Marie Pédrot2013-12-01
| * Ensuring the right parsing of glob arguments, used by refineGravatar Pierre-Marie Pédrot2013-12-01
| * Fixing ltac constr variable handling in refine.Gravatar Pierre-Marie Pédrot2013-11-30
| * Adding printing of ltac envs to debugger.Gravatar Pierre-Marie Pédrot2013-11-30
| * Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30