aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-12-19test-suite/output/Notations : evar number changePierre Boutillier
2013-12-19Bad use of Obj.magic in interpretation of TacAlias arguments.Pierre Boutillier
2013-12-19Printing function for Stdargs in debuggerPierre Boutillier
2013-12-19Missing Fail in r16792Pierre Boutillier
2013-12-17test guard condition against feature incompatible with prop-extBruno Barras
2013-12-17Fix make install after 3e972b3ff8e532be233f70567c87512324c99b4ePierre Boutillier
2013-12-17Merge branch 'trunk' of github.com:coq/coq into trunkMatthieu Sozeau
2013-12-17Tentative fix of the guardedness checker by Christine and me. All stdlib and ...Matthieu Sozeau
2013-12-17Removing the need of evarmaps in constr internalization.Pierre-Marie Pédrot
2013-12-16Get rid of messages "emitting ..." when compiling .v filesPierre Letouzey
2013-12-16A few fixes to the build system (mostly for ocamlbuild)Pierre Letouzey
2013-12-16Added test-suite for bug #2990.Pierre-Marie Pédrot
2013-12-16Dedicated inductive for return values of rewrite strategies.Pierre-Marie Pédrot
2013-12-15Do not overallocate closures' named environments in infos. Modifying the accessPierre-Marie Pédrot
2013-12-12Do not compile coqide with -threadPierre Boutillier
2013-12-12Patch for supporting [From Xxx Require Yyy Zzz.]Gregory Malecha
2013-12-12Better unification for [projT1] and [proj1_sig].Jason Gross
2013-12-12Generalize eq_proofs_unicityJason Gross
2013-12-11Documenting the tactic-in-term construction.Pierre-Marie Pédrot
2013-12-11Fix CoqIDE compilation under standard version of lablgtk2Enrico Tassi
2013-12-11Fixing backtrace registering of various tactic-related try-with blocks.Pierre-Marie Pédrot
2013-12-10Fix CoqIDE on windowsEnrico Tassi
2013-12-10Renaming elisp files to avoid conflict with pg in distribs.Pierre Courtieu
2013-12-09Fix printing of Ltac's backtrace.Arnaud Spiwack
2013-12-09Stylistic change.Arnaud Spiwack
2013-12-06Fix test-suite/success/evars.v.Arnaud Spiwack
2013-12-06Remove duplicate test-suite file.Arnaud Spiwack
2013-12-06Fix the refine related test-suite files to account for the new refine.Arnaud Spiwack
2013-12-06Missing file in commit 1fb883.Arnaud Spiwack
2013-12-04Fix g_derive.ml4.Arnaud Spiwack
2013-12-04Documentation of the Derive plugin.Arnaud Spiwack
2013-12-04Stm: remove an assertion.Arnaud Spiwack
2013-12-04Derive plugin.Arnaud Spiwack
2013-12-04Fix Admitted.Arnaud Spiwack
2013-12-04Proof_global: fix start_proof comment after the preceding commits.Arnaud Spiwack
2013-12-04Factoring(continued).Arnaud Spiwack
2013-12-04Refactoring: storing more information in the terminator closure.Arnaud Spiwack
2013-12-04The commands that initiate proofs are now in charge of what happens when proo...Arnaud Spiwack
2013-12-04Vernac classification: allow for commands which start proofs but must be sync...Arnaud Spiwack
2013-12-04Allow proofs to start with dependent goals.Arnaud Spiwack
2013-12-04Improved the presentation of the proof of UIP_refl_nat.Hugo Herbelin
2013-12-04Add lemma derivable_pt_lim_atan.Guillaume Melquiond
2013-12-03Removing useless meta-related functions.Pierre-Marie Pédrot
2013-12-03Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Guillaume Melquiond
2013-12-03Silence some warning about references in documentation.Guillaume Melquiond
2013-12-03Remove a useless hypothesis from Rle_Rinv.Guillaume Melquiond
2013-12-03Ensure locality modifiers are properly highlighted in CoqIDE.Guillaume Melquiond
2013-12-03Silence compilation warning by avoiding some deprecated constructs.Guillaume Melquiond
2013-12-02Test case for bug#2848.xclerc
2013-12-02Porting type interpretation in Tacinterp to the new tactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-20 05:54:51 +0000