aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-06-23Change the proj_ind field from MutInd.t to inductive.Pierre-Marie Pédrot
2018-06-23Merge PR #7715: Simplify the cooking of primitive projections.Maxime Dénès
2018-06-22Merge PR #7600: Faster and cleaner fconstr-to-constr conversion function.Maxime Dénès
2018-06-22Merge PR #7893: Update dpdgraph branch nameThéo Zimmermann
2018-06-22Merge PR #7776: [ssr] Fix rewrite with universesMaxime Dénès
2018-06-22Fix #7704: get_toplevel_path needs normalised argv.(0)Gaëtan Gilbert
2018-06-22Fix handling of universe context for expanded program obligations.Matthieu Sozeau
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
2018-06-22Define and use UGraph.enforce_leq_alg for subtyping inferenceGaëtan Gilbert
2018-06-22[ssr] document {}/viewEnrico Tassi
2018-06-22[ssr] document rewrite {}fooEnrico Tassi
2018-06-22[ssr] implement {}/v as a short hand for {v}/v when v is an idEnrico Tassi
2018-06-22[ssr] simplify delayed clearsEnrico Tassi
2018-06-22[ssr] test case for rewrite and set on univ poly keysEnrico Tassi
2018-06-22[ssr] matching: use eq_constr_nounivs in approximated matchingEnrico Tassi
2018-06-22[ssr] set: merge universe constraints before type checking the termEnrico Tassi
2018-06-22Revert "Add a note about [ci skip] in CI README."Théo Zimmermann
2018-06-22Get rid of INSTALL.ide. List the dependency versions in INSTALL.Théo Zimmermann
2018-06-22Fix #7608: missing num package in INSTALL documentation.Théo Zimmermann
2018-06-22Fix Windows install script following removal of INSTALL.ide and move of INSTA...Théo Zimmermann
2018-06-22Clarify further doc/README.md following Jim's comments.Théo Zimmermann
2018-06-22Fix copyright dates in doc/LICENSE.Théo Zimmermann
2018-06-22Improve doc/README.md.Théo Zimmermann
2018-06-22Move INSTALL.doc into doc/README.md.Théo Zimmermann
2018-06-21Merge PR #7774: [build] Fix checks and notes noting 4.02.1 instead of 4.02.3Maxime Dénès
2018-06-21Merge PR #7873: Make Clément the secondary codeowner of doc/tools/coqrst.Maxime Dénès
2018-06-21Update dpdgraph branch nameGaëtan Gilbert
2018-06-21Merge PR #7770: Move indices on top on the TOC. Closes #7764.Maxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-04 16:39:43 +0000