aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker
Commit message (Expand)AuthorAge
* Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...Gravatar Matthieu Sozeau2018-06-04
|\
* | Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
* | Merge PR #7325: Fix #7323: coqchk puts polymorphic univs of inductive in glob...Gravatar Pierre-Marie Pédrot2018-05-25
|\ \
* \ \ Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...Gravatar Pierre-Marie Pédrot2018-05-24
|\ \ \
| | * | Fix #7323: coqchk puts polymorphic univs of inductive in global envGravatar Gaëtan Gilbert2018-05-24
| |/ / |/| |
* | | Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constantsGravatar Pierre-Marie Pédrot2018-05-24
|\ \ \
* \ \ \ Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant inst...Gravatar Pierre-Marie Pédrot2018-05-24
|\ \ \ \
| | | * | Moving Rtree.smart_map into Rtree.Smart.map.Gravatar Hugo Herbelin2018-05-23
| | | * | Moving Option.smart_map to Option.Smart.map.Gravatar Hugo Herbelin2018-05-23
| | | * | Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
| | | * | Collecting Array.smart_* functions into a module Array.Smart.Gravatar Hugo Herbelin2018-05-23
| |_|/ / |/| | |
| | | * Fix #7539: Checker does not properly handle negative coinductive types.Gravatar Pierre-Marie Pédrot2018-05-18
* | | | Infrastructure for ocamldebug on the checkerGravatar Gaëtan Gilbert2018-05-13
| |_|/ |/| |
| | * Fix #7327: coqchk subtyping of polymorphic constantsGravatar Gaëtan Gilbert2018-04-23
| |/
| * Fix #6798: coqchk ignores ugraph when comparing constant instancesGravatar Gaëtan Gilbert2018-04-20
|/
* [api] Deprecate a couple of aliases that we missed.Gravatar Emilio Jesus Gallego Arias2018-03-28
* Merge PR #6800: [checker] Printer cleanup.Gravatar Maxime Dénès2018-03-09
|\
* | Update checker to reflect rule on constructors of polymorphic inductive typesGravatar Matthieu Sozeau2018-03-08
| * [checker] Printer cleanup.Gravatar Emilio Jesus Gallego Arias2018-03-07
|/
* Replace invalid tag @raises in ocamldoc comments with @raiseGravatar mrmr19932018-03-05
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* \ Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Maxime Dénès2018-02-28
|\ \
| | * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
| |/ |/|
* | 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
|\ \ \
| | | * dest_{prod,lam}: no Cast case (it's removed by whd)Gravatar Gaëtan Gilbert2018-02-11
| | |/
* | / 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 02:25:02 +0000