aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-07-03closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Pierre Letouzey
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-07-01Merge branch 'reduction-flags' into trunkMaxime Dénès
2016-07-01Add and document match, fix and cofix reduction flags.Maxime Dénès
2016-07-01Make semantics of whd_zeta consistent with other whd_* functions.Maxime Dénès
2016-07-01Separate flags for fix/cofix/match reduction and clean reduction function names.Maxime Dénès
2016-06-29Fixing #4865 (deciding on which arguments to recompute scopes was not robust).Hugo Herbelin
2016-06-29Exporting section_segment_of_reference.Hugo Herbelin
2016-06-29Updated CHANGES about subst. More on recursive equations in reference manual.Hugo Herbelin
2016-06-29Merge branch 'programcases' into trunkMatthieu Sozeau
2016-06-29Fixes in documentation.Matthieu Sozeau
2016-06-29Program: cleanup in cases, add optionsMatthieu Sozeau
2016-06-29Merge branch 'bug4527' into trunkMatthieu Sozeau
2016-06-29Univ: Use loc even if there are more unbound levelsMatthieu Sozeau
2016-06-29CHANGES: document fix for #4726 too.Matthieu Sozeau
2016-06-29CHANGES: document fix for 4527 and compatibility.Matthieu Sozeau
2016-06-29universes.ml: Minor code cleanupMatthieu Sozeau
2016-06-29Univs: Fix bug #4726Matthieu Sozeau
2016-06-29Univs: add source locations of levelsMatthieu Sozeau
2016-06-29Univs: earlier errors for strict univ decls #4527Matthieu Sozeau
2016-06-29Merge branch 'warnings' into trunkMaxime Dénès
2016-06-29Fix issues in test-suite revealed by warnings.Maxime Dénès
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-29Add [Unset Printing Dependent Evars Line]Jason Gross
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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 02:42:39 +0000