aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Collapse)AuthorAge
* Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\
| * deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| |
* | Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
|/ | | | | | | | | | | | | The use of template polymorphism in constants was quite limited, as it only applied to definitions that were exactly inductive types without any parameter whatsoever. Furthermore, it seems that following the introduction of polymorphic definitions, the code path enforced regular polymorphism as soon as the type of a definition was given, which was in practice almost always. Removing this feature had no observable effect neither on the test-suite, nor on any development that we monitor on Travis. I believe it is safe to assume it was nowadays useless.
* Fixing the checker w.r.t. wrongly used abstract universe contexts.Gravatar Pierre-Marie Pédrot2017-07-19
| | | | | | | | | | | It seems we were not testing the checker on cumulative inductive types, because judging from the code, it would just have exploded in anomalies. Before this patch, the checker was mixing De Bruijn indices with named variables, resulting in ill-formed universe contexts used throughout the checking of cumulative inductive types. This patch also gets rid of a lot of now dead code, and removes abstraction breaking code from the checker.
* Properly handling polymorphic inductive subtyping in the checker.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | This is the followup of the previous commit, this time implementing the correct algorithm in the checker.
* Safe API for accessing universe constraints of global references.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | Instead of returning either an instance or the set of constraints, we rather return the corresponding abstracted context. We also push back all uses of abstraction-breaking calls from these functions out of the kernel.
* Less footguns in universe handling: remove subst_instance_context.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | This function was lurking around, waiting to bite anybody willing to use it. We use instead a better API, correct and much less error-prone.
* Getting rid of simple calls to AUContext.instance.Gravatar Pierre-Marie Pédrot2017-07-11
| | | | | | This function breaks the abstraction barrier of abstract universe contexts, as it provides a way to observe the bound names of such a context. We remove all the uses that can be easily get rid of with the current API.
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* A short cleanupGravatar Amin Timany2017-06-16
|
* use map_constr more efficientlyGravatar Amin Timany2017-06-16
|
* OptimizationGravatar Amin Timany2017-06-16
| | | | | Only try using cumulativity in conversion/subtyping if the universe instances are non-empty
* Use a smart map_constrGravatar Amin Timany2017-06-16
|
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
|
* Checker add test for non-trivial constraintsGravatar Amin Timany2017-06-16
|
* Properly instantiate contexts before pushingGravatar 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
|
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\
* | 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 ```
* | Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\ \
| | * Fix a bug in checkerGravatar Amin Timany2017-05-28
| | | | | | | | | | | | Universe constraints of the inductive types were not instantiated before being pushed on the environment. This commit fixes this bug.
| * | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is the continuation of #244, we now deprecate `CErrors.error`, the single entry point in Coq is `user_err`. The rationale is to allow for easier grepping, and to ease a future cleanup of error messages. In particular, we would like to systematically classify all error messages raised by Coq and be sure they are properly documented. We restore the two functions removed in #244 to improve compatibility, but mark them deprecated.
* | | [checker] [votour] resolve warning 52 fragile constant patternGravatar Gaëtan Gilbert2017-05-26
| | | | | | | | | | | | Also stop using failwith for flow control in tuple_of_string.
* | | [votour] Fix/disable warnings.Gravatar Emilio Jesus Gallego Arias2017-05-26
| | |
* | | [votour] Fix build with -safe-string (bug 5553)Gravatar Emilio Jesus Gallego Arias2017-05-26
|/ /
* | Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| * \ Merge PR#411: Mention template polymorphism in the documentation.Gravatar Maxime Dénès2017-05-03
| |\ \
| * \ \ Merge PR#582: Fix warningsGravatar Maxime Dénès2017-05-02
| |\ \ \
| * | | | More consistent writing of de Bruijn.Gravatar Théo Zimmermann2017-05-01
| | | | |
| | * | | Remove uses of [Flags.make_silent]Gravatar Gaetan Gilbert2017-04-27
| | | | |
| | * | | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | | | |
| | * | | Remove unused [rec] keywordsGravatar Gaetan Gilbert2017-04-27
| | | | |
| | * | | Locally disable some warnings.Gravatar Gaetan Gilbert2017-04-27
| |/ / /
* / / / [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
|/ / / | | | | | | | | | Now it is a private field, locations are optional.
| * / Update various comments to use "template polymorphism"Gravatar Gaetan Gilbert2017-04-11
|/ / | | | | | | Also remove obvious comments.
* | [pp] Remove uses of expensive string_of_ppcmds.Gravatar Emilio Jesus Gallego Arias2017-03-21
| | | | | | | | | | | | | | In general we want to avoid this as much as we can, as it will need to make choices regarding the output backend (width, etc...) and it is expensive. It is better to serve the printing backends the pretty print document itself.
* | Moving unused code out of the kernel into Termops.Gravatar Pierre-Marie Pédrot2016-10-31
| | | | | | | | | | | | | | Strangely enough, the checker seems to rely on an outdated decompose_app function which is not the same as the kernel, as the latter is sensitive to casts. Cast-manipulating functions from the kernel are only used on upper layers, and thus was moved there.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
| * Merge remote-tracking branch 'github/pr/257' into v8.6Gravatar Maxime Dénès2016-09-30
| |\ | | | | | | | | | Was PR#257: [checker] Fix/fine tune printing.
| * | fix bug 3683 : adds references to the web site for the bug trackerGravatar Yves Bertot2016-09-29
| | | | | | | | | | | | in error messages
* | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \
| * | | Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | | | | | | | | | Suggested by @ppedrot
| * | | Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| | | | | | | | | | | | | | | | | | | | | | | | | | | | As noted by @ppedrot, the first is redundant. The patch is basically a renaming. We didn't make the component optional yet, but this could happen in a future patch.
| * | | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In some cases prior to this patch, there were two cases for the same error function, one taking a location, the other not. We unify them by using an option parameter, in the line with recent changes in warnings and feedback. This implies a bit of clean up in some places, but more importantly, is the preparation for subsequent patches making `Loc.location` opaque, change that could be use to improve modularity and allow a more functional implementation strategy --- for example --- of the beautifier.
| | * [checker] Fix/fine tune printing.Gravatar Emilio Jesus Gallego Arias2016-08-18
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | In 91ee24b4a7843793a84950379277d92992ba1651 , we discouraged direct access to the console, recommending instead to provide information to the user by means of the `Feedback.msg_*` facilities. However, we introduced a display bug in the checker printer as it is special and doesn't use the Pp facilities (likely for trust reasons), spotted by @herbelin This patch fixes this bug and performs a couple more of fine tunings in the input. However, it could be desirable to port the `checker/printer.ml` to `Pp` and use the feedback mechanism; this would allow IDEs to use the checker in a more convenient way, at the cost of trusting `Pp` (which is already a bit trusted currently) A start of that idea can be found at: https://github.com/ejgallego/coq/tree/fix_checker_printing
* / remove checker/MakefileGravatar Pierre Letouzey2016-07-26
|/ | | | | | This historical Makefile was used during the development of coqcheck, but was unused since then : the checker is built via Coq's main Makefile. So let's remove this one to avoid any risk of confusion.
* Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-26
|\
| * Fix bug #4876: critical bug in guard condition checker.Gravatar Matthieu Sozeau2016-07-25
| |