aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-06-29Add [Unset Printing Dependent Evars Line]Jason Gross
2016-06-28fix coqide double module linking (error on OCaml 4.03)Gabriel Scherer
2016-06-28Revert "A new infrastructure for warnings."Maxime Dénès
2016-06-28Typeclasses: use once in by clause for typeclass eautoMatthieu Sozeau
2016-06-28Merge branch 'warnings' into trunkMaxime Dénès
2016-06-28A new infrastructure for warnings.Maxime Dénès
2016-06-28Merge remote-tracking branch 'github/pr/207' into trunkMaxime Dénès
2016-06-28Merge branch 'forhott' into v8.5Matthieu Sozeau
2016-06-28Finalizing the only printing feature.Pierre-Marie Pédrot
2016-06-28Documenting the "only printing" notation flag.Pierre-Marie Pédrot
2016-06-28Adding a test-suite for the only printing flag.Pierre-Marie Pédrot
2016-06-28Properly handle the only printing flag in Reserved Notations.Pierre-Marie Pédrot
2016-06-28Properly handling the only printing flag when parsing rules already exist.Pierre-Marie Pédrot
2016-06-27Univs/CHANGES: #4097 and annotations on notationsMatthieu Sozeau
2016-06-27Refine fix for bug #4097, avoid proj expansionMatthieu Sozeau
2016-06-27Univs: allowing notations to take univ instancesMatthieu Sozeau
2016-06-27Forbidding silently dropped universes instances inMatthieu Sozeau
2016-06-27Merge branch 'shrinkobl' into trunkMatthieu Sozeau
2016-06-27Update CHANGES and COMPATIBILITYMatthieu Sozeau
2016-06-27Program: refine shrinking of obligationsMatthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 04:48:34 +0000