aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-06-27Rework treatment of default transparency of obligationsMatthieu Sozeau
2016-06-27Add Unset Shrink Abstract/Obligations in Coq85Matthieu Sozeau
2016-06-27Shrink Proofs/Obligations by default and deprecateMatthieu Sozeau
2016-06-27Typeclasses: fix treatment of exceptions in compatMatthieu Sozeau
2016-06-27Typeclasses: mark unresolvable goals in new implementationMatthieu Sozeau
2016-06-27Fix off-by-1 bug in coq_makefileMatthieu Sozeau
2016-06-27We want tclORELSE to catch exceptions on backtrackingsMatthieu Sozeau
2016-06-27Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-27Merge remote-tracking branch 'github/pr/223' into feedback-locationsMaxime Dénès
2016-06-27ssrmatching: avoid warnings about redundant typing clauses in ARGUMENT EXTENDPierre Letouzey
2016-06-27Merge branch 'sort-fields' into trunkMaxime Dénès
2016-06-27Merge branch 'funpattern-tests' into trunk.Maxime Dénès
2016-06-27minor: comment on the meaning of the 'boolean' variableGabriel Scherer
2016-06-27minor: documentation comment for constrintern.ml:sort_fieldsGabriel Scherer
2016-06-27minor: interp/constrintern.ml, clarify field completionGabriel Scherer
2016-06-27minor: in constrintern.ml:sort_fields, clarify sfGabriel Scherer
2016-06-27add CList.extract_firstGabriel Scherer
2016-06-27minor: in constrintern.ml:sort_fields, clarify build_pattGabriel Scherer
2016-06-27whitespace: untabity constrinternl.ml:sort_fieldsGabriel Scherer
2016-06-27minor clarifications in constrintern.ml:sort_fieldsGabriel Scherer
2016-06-27Patterns in binders: printing testsArnaud Spiwack
2016-06-27Patterns in binders: functional testsArnaud Spiwack
2016-06-27Merge branch 'funpattern' into trunk. Was PR#142: Binder syntax.Maxime Dénès
2016-06-27Adding ability to put any pattern in binders, prefixed by a quote.Daniel de Rauglaudre
2016-06-27More on f9695eb4b, 827663982 on resolving #4782, #4813 (typing "with" clause).Hugo Herbelin
2016-06-27Fix bug #4698: CoqIDE error dialogs piling up when coqtop dies.Pierre-Marie Pédrot
2016-06-25[xmlproto] Remove duplicated deserialization.Emilio Jesus Gallego Arias
2016-06-25[doc] Update changes for feedback.Emilio Jesus Gallego Arias
2016-06-25[feedback] Remove `ErrorMsg` in favor of `Message Error`.Emilio Jesus Gallego Arias
2016-06-25[feedback] Allow messages to carry a location.Emilio Jesus Gallego Arias
2016-06-25[feedback] Add optional ?loc parameter to loggers.Emilio Jesus Gallego Arias
2016-06-25[feedback] Remove unused tag on `Debug` level.Emilio Jesus Gallego Arias
2016-06-25[merlin] Fix .merlin STM includes.Emilio Jesus Gallego Arias
2016-06-24Several easy but efficient optimizations for subst and clear tactics.Pierre-Marie Pédrot
2016-06-24Optimize the subst tactic.Pierre-Marie Pédrot
2016-06-24Optmimize the subst tactic.Pierre-Marie Pédrot
2016-06-24Optim in Clenv: use noccurn instead of depends.Pierre-Marie Pédrot
2016-06-24Optimize the subst tactic.Pierre-Marie Pédrot
2016-06-24Optimize the clear tactic.Pierre-Marie Pédrot
2016-06-24Optimize the clear tactic.Pierre-Marie Pédrot
2016-06-24Optimization in the subst tactic.Pierre-Marie Pédrot
2016-06-24Optimization in the subst tactic.Pierre-Marie Pédrot
2016-06-24Optimization in the subst tactic.Pierre-Marie Pédrot
2016-06-24Removing tactic compatibility layers in setoid_ring.Pierre-Marie Pédrot
2016-06-24Fixing #4854 (regression introduced in 4d25b224 in relation with #4592).Hugo Herbelin
2016-06-24Makefile.install: fix a typo in last commit c954bb5, sorryPierre Letouzey
2016-06-24remove an old workaround for OCaml 3.11 + MacOS natdynlinkPierre Letouzey
2016-06-24Makefile.build: mitigate potential issues with multiple creations of pack .cmiPierre Letouzey
2016-06-24Makefile.install: fix the install of plugin cmiPierre Letouzey
2016-06-23Better algorithm for variable deambiguation in term printing.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 04:14:22 +0000