aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
- we always rename - we compile {clear}/view to /view{clear}
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
This reverts commit 3a44a190a7f5d057b6a4bcb50124b42d83f3d03d.
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 ↵Théo Zimmermann
INSTALL.doc.
2018-06-22Clarify further doc/README.md following Jim's comments.Théo Zimmermann
Relative links. Cf. #7800.
2018-06-22Fix copyright dates in doc/LICENSE.Théo Zimmermann
[ci skip]
2018-06-22Improve doc/README.md.Théo Zimmermann
- Fix the Markdown. - Add link to latest build of the refman for the master branch. - Clarify what are the dependencies of the HTML doc. [ci skip]
2018-06-22Move INSTALL.doc into doc/README.md.Théo Zimmermann
This will avoid in particular this ambiguous file extension. [ci skip]
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
See https://github.com/Karmaki/coq-dpdgraph/issues/50 for context
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
We only use it locally, so we simply register the ML tactic inside the module but we do not export the syntax.
2018-06-21Merge PR #7815: On cygwin, pass the filename in a format that coqdoc ↵Maxime Dénès
understands.
2018-06-21Inline a function from Quote used in setoid_ring.Pierre-Marie Pédrot
The code was wrong as it relies once again on term equality and fails on polymorphic constants. Quote is bound to disappear, so we write a correct version of this 10-line function in setoid_ring.
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 ↵Pierre Courtieu
forward-line.
2018-06-21Merge PR #7880: Clean up DynPierre-Marie Pédrot
2018-06-21Fix #5719: Uncaught exception Invalid_argument.Pierre-Marie Pédrot
It seems that lifting a term with a negative index is not equivalent to strengthening it by applying to a dummy substitution. This looks suspicious at best.
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
We put it in a footnote otherwise the sentence was starting to be really long. Footnotes need to be in index.rst to really appear at the bottom of the index page.
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 ↵Emilio Jesus Gallego Arias
directory
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
I think the bug was introduces when apply_type was made safe. In the test joint to #7255 rewrite (setoid case) generates an ill-typed goal and apply_type raises a Pretype_error. It is unclear to me why the tactic monad does not turn the pretype_error into a UserError
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
There's probably a proof of false using subtyping if someone wants to look. NB: the checker doesn't handle algebraics on the right.
2018-06-19[coqtop] Give priority to stdlib load path over current directoryMaxime Dénès
When initilazing the load path, coqtop adds implicit bindings for stdlib and for the current directory (-R stdlib Coq -R . ""). In case of a clash, the binding of the current directory had priority, which makes it impossible to edit stdlib files (when they Require files from the same directory) using PG, or from CoqIDE when launched from the directory containing the file. Example to reproduce the problem: ``` cd plugins/omega coqide Omega.v ``` some of the Requires will fail.
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 ↵Enrico Tassi
induction schemes
2018-06-19Merge PR #7841: Remove CanaryPierre-Marie Pédrot
2018-06-19[doc] Rewrite and document the prodn directiveClément Pit-Claudel
It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-13 19:56:30 +0000