aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-03-28Patterns: Accepting patterns in PFix and PCofix and not only constr.Hugo Herbelin
2018-03-28Adding Array.fold_left4.Hugo Herbelin
2018-03-28Detyping: Adding a variant of share_names for patterns.Hugo Herbelin
2018-03-28Detyping: Making detype_fix/detype_cofix polymorphic combinator (step 1).Hugo Herbelin
2018-03-28Patternops: renaming an internal function to more closely match its effect.Hugo Herbelin
2018-03-28Glob_ops: cosmetic renaming to reflect the type of objects.Hugo Herbelin
2018-03-28Getting rid of some false "collision between bound variable names" warnings.Hugo Herbelin
2018-03-28Fix #7101: STM delegation policy brokenMaxime Dénès
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-03-28Merge PR #7090: stm: don't propagate side effects when editing a proofEmilio Jesus Gallego Arias
2018-03-28coqide: avoid marking sentences that are not in the document anymoreEnrico Tassi
2018-03-28Merge PR #6961: [test-suite] Add backtracking test for `Load`.Enrico Tassi
2018-03-27stm: don't propagate side effects when editing a proofEnrico Tassi
2018-03-27Adding tacticals tclBINDFIRST/tclBINDLAST.Hugo Herbelin
2018-03-27Export Proofview.undefined as "unsafe" primitive.Hugo Herbelin
2018-03-27Adding informative variant of shelve_unifiable returning set of shelved evars.Hugo Herbelin
2018-03-27Congruence: Fixing a bug with native projections.Hugo Herbelin
2018-03-27Congruence: typography in a comment.Hugo Herbelin
2018-03-27Congruence: getting rid of a detour by the compatibility layer of proof engine.Hugo Herbelin
2018-03-27[default.nix] Unpin nixpkgsMaxime Dénès
2018-03-27Merge PR #6835: Deprecate undocumented "intros until 0" in favor of "intros *"Pierre-Marie Pédrot
2018-03-27Merge PR #7062: Slightly refining some error messages about unresolvable evars.Pierre-Marie Pédrot
2018-03-27Expliciting and taking advantage of a representation invariant in Esubst.Pierre-Marie Pédrot
2018-03-27Adding a fiat-parser overlayHugo Herbelin
2018-03-27Fixing #5547 (typability of return predicate in nested pattern-matching).Hugo Herbelin
2018-03-27Fixing #5500 (missing test in return clause of match leading to anomaly).Hugo Herbelin
2018-03-27Fix printing of toplevel record values.Pierre-Marie Pédrot
2018-03-27Fixup strict mode for patternsPierre-Marie Pédrot
2018-03-26Fixes #7011 (Fix/CoFix were not considered in tactic unification).Hugo Herbelin
2018-03-26[doc] Port Chapter 20 Type Classes to SphinxMatthieu Sozeau
2018-03-26Merge PR #6739: Tentative fix for #6520: camlcity.org unresponsive makes AppV...Maxime Dénès
2018-03-26Move Classes.tex to type-classes.rstMatthieu Sozeau
2018-03-26Merge PR #6970: [vernac] Move `Quit` and `Drop` to the toplevel layer.Enrico Tassi
2018-03-26Add Michael Soegtrop as a code owner for Windows build scripts.Théo Zimmermann
2018-03-26Use Pierre Corbineau GitHub nickname in CODEOWNERS.Théo Zimmermann
2018-03-26More efficient reallocation of VM global tables.Pierre-Marie Pédrot
2018-03-26Moving the VM global atom table to a ML reference.Pierre-Marie Pédrot
2018-03-26Moving the VM global data to a ML reference.Pierre-Marie Pédrot
2018-03-25Clarify wording in tactics documentation.Théo Zimmermann
2018-03-24Slightly refining some error messages about unresolvable evars.Hugo Herbelin
2018-03-23Deprecate undocumented "intros until 0" in favor of "intros *".Hugo Herbelin
2018-03-23Merge PR #7046: Switch maintainers for documentationThéo Zimmermann
2018-03-23Merge PR #7018: Fix typo in CHANGES.Maxime Dénès
2018-03-23Merge PR #7029: improve merge-pr scriptMaxime Dénès
2018-03-23improve merge-pr scriptEnrico Tassi
2018-03-23Merge PR #7052: More precise wording about the merge process.Théo Zimmermann
2018-03-23More precise wording about the merge process.Maxime Dénès
2018-03-23Merge PR #7028: Fix #7026: ssr: applying an overloaded lemma as a view takes ...Enrico Tassi
2018-03-23Merge PR #6968: [stm] Never consider `Backtrack` as part of the script.Enrico Tassi
2018-03-23Merge PR #7025: Coq makefile: provide variables to extend the flags passed to...Enrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 04:45:12 +0000