aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/univ.ml
Commit message (Collapse)AuthorAge
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
|
* Enable the checking of ind subtyping in checkerGravatar Amin Timany2017-06-16
|
* Correct coqchk checking subtyping relation for inductivesGravatar Amin Timany2017-06-16
|
* Correct coqchk reductionGravatar Amin Timany2017-06-16
|
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | | | | | | | | | | | | | | | | As per https://github.com/coq/coq/pull/716#issuecomment-305140839 Partially using ```bash git grep --name-only 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*[^\.!]")' | xargs sed s'/\(anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp.\)\?(\(\(Pp.\)\?str\)\?\s*".*\s*[^\.! ]\)\s*")/\1.")/g' -i ``` and ```bash git grep --name-only ' !"' | xargs sed s'/ !"/!"/g' -i ``` The rest were manually edited by looking at the results of ```bash git grep anomaly | grep '\.ml' | grep -v 'anomaly\s*\(~label:"[^"]*"\s*\)\?\(Pp\.\)\?(\(\(Pp.\)\?str\)\?\s*".*\(\.\|!\)")' | grep 'anomaly\($\|[^_]\)' | less ```
* Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
|
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib ↵Gravatar Pierre Letouzey2016-07-03
| | | | | | module) For the moment, there is an Error module in compilers-lib/ocamlbytecomp.cm(x)a
* A patch renaming equal into eq in the module dealing withGravatar Hugo Herbelin2016-03-22
| | | | | hash-consing, so as to avoid having too many kinds of equalities with same name.
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
|
* Univs: fix checker generating undeclared universes.Gravatar Matthieu Sozeau2015-10-02
|
* Univs: update checkerGravatar Matthieu Sozeau2015-10-02
|
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| | | | | | | | | | | | | | | | | | | | | | Sorry so much. Reverted: 707bfd5719b76d131152a258d49740165fbafe03. 164637cc3a4e8895ed4ec420e300bd692d3e7812. b9c96c601a8366b75ee8b76d3184ee57379e2620. 21e41af41b52914469885f40155702f325d5c786. 7532f3243ba585f21a8f594d3dc788e38dfa2cb8. 27fb880ab6924ec20ce44aeaeb8d89592c1b91cd. fe340267b0c2082b3af8bc965f7bc0e86d1c3c2c. d9b13d0a74bc0c6dff4bfc61e61a3d7984a0a962. 6737055d165c91904fc04534bee6b9c05c0235b1. 342fed039e53f00ff8758513149f8d41fa3a2e99. 21525bae8801d98ff2f1b52217d7603505ada2d2. b78d86d50727af61e0c4417cf2ef12cbfc73239d. 979de570714d340aaab7a6e99e08d46aa616e7da. f556da10a117396c2c796f6915321b67849f65cd. d8226295e6237a43de33475f798c3c8ac6ac4866. fdab811e58094accc02875c1f83e6476f4598d26.
* Hconsing continuedGravatar Hugo Herbelin2015-08-02
|
* Fixing bug #4019, and checker blow-up at once.Gravatar Pierre-Marie Pédrot2015-02-11
|
* Clarifying the implementation of universe hashconsing.Gravatar Pierre-Marie Pédrot2015-02-11
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Fix checker's treatment of template polymorphicGravatar Matthieu Sozeau2015-01-06
| | | | | inductive instantiation, now using substitution of levels. Fixes the test-suite file coqchk/univ.
* Backporting the change in lists of universes to the checker.Gravatar Pierre-Marie Pédrot2014-12-18
|
* checker: Change in library on disk values, now using context_sets instead ofGravatar Matthieu Sozeau2014-12-17
| | | | constraints only.
* Ensuring the good invariants of hashcons table generation in the API.Gravatar Pierre-Marie Pédrot2014-12-17
|
* Remove unused substitution functions in checker.Gravatar Matthieu Sozeau2014-09-05
|
* Fix checker treatment of inductives using subst_instances instead of ↵Gravatar Matthieu Sozeau2014-09-05
| | | | subst_univs_levels.
* Removing dead code in checker/univ.ml.Gravatar Pierre-Marie Pédrot2014-06-10
|
* Removing explanations of universe inconsistencies from the checker. TheyGravatar Pierre-Marie Pédrot2014-06-10
| | | | were never used and were responsible for code duplication.
* Providing the checker with its own version of the Univ file.Gravatar Pierre-Marie Pédrot2014-06-10
I also took the opportunity to remove a lot of code not used by the checker.