aboutsummaryrefslogtreecommitdiff
path: root/etc
AgeCommit message (Collapse)Author
2021-03-25fix gotpodCyril Cohen
2021-03-15fixup gitpod configCyril Cohen
2020-06-27Fix bugs in hierarchy.mlKazuhiko Sakaguchi
- pass `Unix.environment ()` to `coqtop` to preserve the parent process environment, - check the exit status of `coqtop` and report an error if it is wrong, - do not rely on `ssrfun.id` in the `check_join` tactic, and - improve the error message for missing unification hints.
2020-06-10Generated opam packages allow coq-dev againCyril Cohen
As a result of [a discussion on Zulip](https://coq.zulipchat.com/#narrow/stream/237665-math-comp-devs/topic/MathComp.201.2E11.2E0.20OPAM.20packages.20Coq.20compatibility) Reverts "removing opam `| (= "dev")` for released packages" (commit 313e44316177c918b363c118f15297e08d13eb4e).
2020-06-09removing opam `| (= "dev")` for released packagesCyril Cohen
2020-05-27URL in httpsCyril Cohen
2020-04-15fix packagerCyril Cohen
2020-03-15Fix hierarchy.ml to compute the transitive closure of a hierarchyKazuhiko Sakaguchi
2019-12-02take advantage of opam variables and their default valuesYves Bertot
2019-11-25Add Makefile target to build the docMaxime Dénès
2019-10-02Fix and improve the test suite and MakefileKazuhiko Sakaguchi
- improve an error message produced by the `check_join` tactic, - fix the build of the test suite: `make test-suite`, and - add a new rule `only` to build a subset of MathComp.
2019-04-30Reimplement the hierarchy related tools in OCamlKazuhiko Sakaguchi
The functionalities of the structure hierarchy related tools `hierarchy-diagram` and `hierarchy_test.py` are provided by an OCaml script `hierarchy.ml`. `test_suite/hierarchy_test.v` is deleted. Now make can generate it.
2019-04-08switching to opam 2.0 formatCyril Cohen
2019-04-08New test cases generation: corrent implementation of least common childrenKazuhiko Sakaguchi
Add a new option `-raw-inheritances` to `hierarchy-diagram` to generate an intermediate file for `hierarchy_test.py`. So the typical usage is: $ python3.5 etc/utils/hierarchy_test.py \ <(etc/utils/hierarchy-diagram -raw-inheritances -R mathcomp mathcomp) \ > mathcomp/test_suite/hierarchy_test.v
2019-04-05least common childenCyril Cohen
2019-04-04no output on success in test_suite/hierarchy_test.v (#323)Cyril Cohen
2019-04-02speedup in hierarchy_test.pyCyril Cohen
2019-04-02identifying missing joinsCyril Cohen
2019-03-07Put documentation and some command line options for hierarchy-diagramKazuhiko Sakaguchi
2019-03-07Use both coercions and canonical projections to generate the diagramKazuhiko Sakaguchi
2019-02-22Reimplement hierarchy-diagram by using coercions between "<module>.type" typesKazuhiko Sakaguchi
2019-02-22Add a tool to draw the hierarchy diagramKazuhiko Sakaguchi
2019-02-05fix etc/utils/packager (#273)Cyril Cohen
2018-04-24replacing my local `git root` by a universal commandCyril Cohen
2018-04-24fix opam packager script + dependenciesCyril Cohen
2018-04-20move etc/ files to the root and remove obsolete onesEnrico Tassi
2017-10-23Remove compatibility with Coq.8.4 (and compatibility hacks that went with it)Cyril Cohen
2017-10-23Merge pull request #145 from CohenCyril/new-packagerCyril Cohen
New packager
2017-10-20reproduce github archive locally rather than downloading, much fasterCyril Cohen
2017-10-20improved package generatorCyril Cohen
2017-10-19new script to create opam meta packagesCyril Cohen
- the opam files in the branch where the script is launched should be correct - if not, the second argument to the script should be a branch in which the opam files are correct
2017-10-19No more `cm*` files in the installer!Enrico
Since they are all in Coq!
2017-09-07extended changelog in preparation for the next releaseCyril Cohen
2017-09-07adding odd_order to the list of released content for 1.6Cyril Cohen
2016-10-25minor change to the opam install exampleFalcon Dai
fix a typo in the example command add `opam repo add coq-released http://coq.inria.fr/opam/released`
2016-08-25Enriched numClosedFieldType so that it factors a lot of theory from both ↵Cyril Cohen
complex and algC. The definitions of 'i, conjC, Re, Im, n.-root, sqrtC and their theory have been moved to the numClosedFieldType structure in ssrnum. This covers boths the uses in algC and complex.v. To that end the numClosedFieldType structure has been enriched with conjugation and 'i. Note that 'i can be deduced from the property of algebraic closure and is only here to let the user chose which definitional equality should hold on 'i. Same thing for conjC that could be written `|x|^+2/x, the only nontrivial (up to my knowledge) property is the fact that conjugation is a ring morphism.
2016-03-02Fix the address if the wiki. Florent Hivert
The previous fix wasn't right.
2016-01-21revise installer for windowsEnrico Tassi
2016-01-05do not use `sed -i' in ssrcoqdep -- this is not portablePierre-Yves Strub
This prevents compilation of ssreflect on OS-X/*BSD.
2015-12-26packaging ssr 1.6Cyril Cohen
2015-12-18Changing the address of the wikiamahboubi
2015-12-18Typo in the github announceamahboubi
2015-12-15Update ANNOUNCE-1.6.mdEnrico
2015-12-14typoEnrico Tassi
2015-12-14Update ANNOUNCE-github.mdEnrico
2015-12-12typoCyril Cohen
2015-12-12modif packager ":" -> "-"Cyril Cohen
2015-12-118.5 coqdoc does not want _ to be escaped + more .css classesEnrico Tassi
2015-12-10some doc for the doc building utilityEnrico Tassi
2015-12-09Updated the address of the website in READMEAssia Mahboubi
Plus corrected some typos.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:20:57 +0000