aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-12-22Slight code cleaning ensuring more static invariants in Rewrite.Pierre-Marie Pédrot
2013-12-22Adding -bt to coqc.Pierre-Marie Pédrot
2013-12-22Adding a finer-grained -bt flag to coqtop only triggering backtraces.Pierre-Marie Pédrot
2013-12-22Notation variables are now taken into account as possible ltac bound variablesPierre-Marie Pédrot
2013-12-22Notations now accept the $(...)$ tactic-in-term syntax. They are resolved atPierre-Marie Pédrot
2013-12-22Notations can now accept dummy arguments. If ever a bound variable is notPierre-Marie Pédrot
2013-12-21Test case for the buggy commutative cut subterm rule.Maxime Dénès
2013-12-20configure.ml: our configure script is now written in ML :-)Pierre Letouzey
2013-12-20Makefile.build: avoid a -ppPierre Letouzey
2013-12-20coqc: execvp is now available even on win32Pierre Letouzey
2013-12-20coqmktop without Unix (simpler all_subdirs)Pierre Letouzey
2013-12-20Remove unused Makefile lines about .elc compilationPierre Letouzey
2013-12-20Warning removalPierre Boutillier
2013-12-20List: Bug 3039 weaker requirement for fold symmetricPierre Boutillier
2013-12-20Coqdep always uses / as dir_sepPierre Boutillier
2013-12-20micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...Frédéric Besson
2013-12-19Removing the useless pattern ident genarg.Pierre-Marie Pédrot
2013-12-19Using interp_genarg in tactic notations where possible, instead of an ad-hocPierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 17:11:21 +0000