aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Expand)AuthorAge
* Merge PR #6740: Adding a sanity check on inductive variance subtyping.Gravatar Maxime Dénès2018-02-21
|\
* \ Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...Gravatar Maxime Dénès2018-02-19
|\ \
* \ \ Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...Gravatar Maxime Dénès2018-02-19
|\ \ \
| * | | Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
| | * | Extrude monomorphic universe contexts from with Definition constraints.Gravatar Pierre-Marie Pédrot2018-02-16
| |/ / |/| |
| | * Adding a sanity check on inductive variance subtyping.Gravatar Pierre-Marie Pédrot2018-02-15
| |/ |/|
* | Merge PR #6262: [error] Replace msg_error by a proper exception.Gravatar Maxime Dénès2018-02-12
|\ \
* | | Simplification: cumulativity information is variance information.Gravatar Gaëtan Gilbert2018-02-10
| |/ |/|
| * [error] Replace msg_error by a proper exception.Gravatar Emilio Jesus Gallego Arias2018-02-09
|/
* checker: cleanup projection unfoldingGravatar Gaëtan Gilbert2018-02-02
* checker: remove unused per-constant reduction flags.Gravatar Gaëtan Gilbert2018-02-02
* [checker] Avoid relying on canonical names.Gravatar Maxime Dénès2018-01-25
* [checker] Remove duplicated functionGravatar Maxime Dénès2018-01-25
* [checker] Better error message for bad recursive treesGravatar Maxime Dénès2018-01-25
* fix space in coqchk errorGravatar Ralf Jung2018-01-24
* Fix #6618: coqchk fails with "ill-typed term".Gravatar Pierre-Marie Pédrot2018-01-20
* Actually use the strategy information in the checker.Gravatar Pierre-Marie Pédrot2018-01-14
* Store the conversion oracle in constant and inductive definitions.Gravatar Pierre-Marie Pédrot2018-01-14
* Add interfaces for checker and remove dead code.Gravatar Maxime Dénès2018-01-10
* Moving some universe substitution code out of the kernel.Gravatar Pierre-Marie Pédrot2017-12-30
* [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
* Merge PR #6277: Qualified import in coqchkGravatar Maxime Dénès2017-12-07
|\
* \ Merge PR #6303: Remove redundant Zcase from the checker.Gravatar Maxime Dénès2017-12-07
|\ \
* \ \ Merge PR #6266: Safe unmarshalling in the checkerGravatar Maxime Dénès2017-12-05
|\ \ \
| | * | Remove redundant Zcase from the checker.Gravatar Pierre-Marie Pédrot2017-12-02
| |/ / |/| |
| | * Documenting the -Q flag of coqchk.Gravatar Pierre-Marie Pédrot2017-12-01
| | * Forbid implicitly relative names in the checker.Gravatar Pierre-Marie Pédrot2017-11-29
| | * Mark the -I option in coqchk as deprecated and merge it with -Q.Gravatar Pierre-Marie Pédrot2017-11-29
| | * Add a -Q option to coqchck.Gravatar Pierre-Marie Pédrot2017-11-29
| |/ |/|
* | Allow to pass physical files to coqchk.Gravatar Pierre-Marie Pédrot2017-11-29
* | Adding an interface file for checker/check.ml.Gravatar Pierre-Marie Pédrot2017-11-28
| * Use safe demarshalling in the checker.Gravatar Pierre-Marie Pédrot2017-11-28
| * Use large arrays in the checker demarshaller.Gravatar Pierre-Marie Pédrot2017-11-28
|/
* Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\
| * When declaring constants/inductives use ContextSet if monomorphic.Gravatar Gaëtan Gilbert2017-11-24
* | Truncate strings in votour to 1024 characters.Gravatar Pierre-Marie Pédrot2017-11-23
* | Bypass int and string representation in votour when it's incorrect.Gravatar Pierre-Marie Pédrot2017-11-23
* | Tail-recursive list traversal in votour.Gravatar Pierre-Marie Pédrot2017-11-23
* | Implement a tail-recursive traversal of the object in votour.Gravatar Pierre-Marie Pédrot2017-11-22
|/
* Merge PR #6065: [api] Deprecate all legacy uses of Names in core.Gravatar Maxime Dénès2017-11-13
|\
| * [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* | [feedback] Helper to print feedback messages in the console.Gravatar Emilio Jesus Gallego Arias2017-11-06
|/
* Merge PR #1075: Re-enable checker error messagesGravatar Maxime Dénès2017-09-25
|\
| * Fix -silent flag of coqchk after ff918e4.Gravatar Maxime Dénès2017-09-21
| * Adapt checker to change in locations.Gravatar Maxime Dénès2017-09-21
| * [checker] Add missing Feedback printer (BZ#5587)Gravatar Emilio Jesus Gallego Arias2017-09-21
* | [flags] Flag `open Flags`Gravatar Emilio Jesus Gallego Arias2017-09-20
|/
* Merge PR #955: Do not hashcons universes beforehandGravatar Maxime Dénès2017-09-15
|\
| * Do not hashcons universes beforehand.Gravatar Pierre-Marie Pédrot2017-09-01
* | Statically enforcing that module types have no retroknowledge.Gravatar Pierre-Marie Pédrot2017-08-29
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 22:37:33 +0000