aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-06-21Further cleanup: do not export the closed_term Ltac entry.Pierre-Marie Pédrot
2018-06-21Merge PR #7815: On cygwin, pass the filename in a format that coqdoc understa...Maxime Dénès
2018-06-21Inline a function from Quote used in setoid_ring.Pierre-Marie Pédrot
2018-06-21Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.Maxime Dénès
2018-06-21Remove enforce_leq from checkerGaëtan Gilbert
2018-06-21Merge PR #7842: Fix #7836: tools/inferior-coq.el uses next-line instead of fo...Pierre Courtieu
2018-06-21Merge PR #7880: Clean up DynPierre-Marie Pédrot
2018-06-21Fix #5719: Uncaught exception Invalid_argument.Pierre-Marie Pédrot
2018-06-21Add documentation for Dyn.whitequark
2018-06-21Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their purpose.whitequark
2018-06-21Reformat Dyn.{ml,mli}.whitequark
2018-06-20Mention Company-Coq as well.Théo Zimmermann
2018-06-20Add a good reference for Proof-General as suggested by Clément.Théo Zimmermann
2018-06-20Modernize the introduction of the reference manual.Théo Zimmermann
2018-06-20On cygwin, pass the filename in a format that coqdoc understands.Jim Fehrle
2018-06-20Merge PR #7868: [coqtop] Give priority to stdlib load path over current direc...Emilio Jesus Gallego Arias
2018-06-20[ssr] test case for rewrite (setoid) making the goal illtypedEnrico Tassi
2018-06-20[ssr] rewrite: turn anomaly into regular errorEnrico Tassi
2018-06-20Make Clément the secondary codeowner of doc/tools/coqrst.Théo Zimmermann
2018-06-19Fix Univ.enforce_leq dropped constraints when algebraic on the rightGaëtan Gilbert
2018-06-19[coqtop] Give priority to stdlib load path over current directoryMaxime Dénès
2018-06-19Merge PR #7797: Remove reference name type.Enrico Tassi
2018-06-19Merge PR #6754: Better elaboration of pattern-matchings on primitive projectionsPierre-Marie Pédrot
2018-06-19Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.Pierre-Marie Pédrot
2018-06-19Merge PR #7801: [vernac] Add option to force building really mutual induction...Enrico Tassi
2018-06-19Merge PR #7841: Remove CanaryPierre-Marie Pédrot
2018-06-19[doc] Rewrite and document the prodn directiveClément Pit-Claudel
2018-06-19[doc] Fix a typo in the ssreflect chapterClément Pit-Claudel
2018-06-19[doc] Fix uncaught duplicate-label errors in the SSReflect chapterClément Pit-Claudel
2018-06-19[doc] Use productionlist instead of prodn in ring.rstClément Pit-Claudel
2018-06-19Merge PR #7714: Remove primitive-projection related data from the kernelMaxime Dénès
2018-06-19Merge PR #7856: Fix #7829: Spurious documentation failures.Maxime Dénès
2018-06-18Overlay for reference removalMaxime Dénès
2018-06-18Adapt to Coq's PR #7797 (removal of reference).Maxime Dénès
2018-06-18Merge PR #7855: Update section on adding your project to CI and link to examp...Emilio Jesus Gallego Arias
2018-06-18Do not rely on the Ident vs. Qualid artificial separation.Pierre-Marie Pédrot
2018-06-18Fixing a batch of deprecation warnings.Pierre-Marie Pédrot
2018-06-18Fix #7421: constr_eq ignores universe constraints.Gaëtan Gilbert
2018-06-18Remove Canary.whitequark
2018-06-18Fix #7829: Spurious documentation failures.Théo Zimmermann
2018-06-18Merge PR #7840: Remove Hashcons.HobjPierre-Marie Pédrot
2018-06-18Update section on adding your project to CI and link to example PR.Théo Zimmermann
2018-06-18Remove reference name type.Maxime Dénès
2018-06-17Remove Hashcons.Hobj.whitequark
2018-06-17Merge PR #7824: Fixes #7811 (uncaught Not_found in notation printer related t...Pierre-Marie Pédrot
2018-06-17Merge PR #7848: Fix a typo in documentationThéo Zimmermann
2018-06-17Merge PR #7822: cArray: proper invalid_arg exceptionsPierre-Marie Pédrot
2018-06-17Remove Tutorial from Additional documentation in refman intro.Théo Zimmermann
2018-06-17Remove Tutorials from doc/LICENSE following #7466.Théo Zimmermann
2018-06-17Merge PR #7844: Remove Elpi from Travis.Emilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-18 16:42:19 +0000