aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2018-03-08Update checker to reflect rule on constructors of polymorphic inductive typesMatthieu Sozeau
2018-03-07[checker] Printer cleanup.Emilio Jesus Gallego Arias
2018-03-05Replace invalid tag @raises in ocamldoc comments with @raisemrmr1993
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-28Merge PR #6734: dest_{prod,lam}: no Cast case (it's removed by whd)Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-21Merge PR #6740: Adding a sanity check on inductive variance subtyping.Maxime Dénès
2018-02-19Merge PR #6728: Extrude monomorphic universe contexts from with Definition co...Maxime Dénès
2018-02-19Merge PR #6646: Change references to CAMLP4 to CAMLP5 since we no longer use ...Maxime Dénès
2018-02-17Change references to CAMLP4 to CAMLP5 to be more accurate since we noJim Fehrle
2018-02-16Extrude monomorphic universe contexts from with Definition constraints.Pierre-Marie Pédrot
2018-02-15Adding a sanity check on inductive variance subtyping.Pierre-Marie Pédrot
2018-02-12Merge PR #6262: [error] Replace msg_error by a proper exception.Maxime Dénès
2018-02-11dest_{prod,lam}: no Cast case (it's removed by whd)Gaëtan Gilbert
2018-02-10Simplification: cumulativity information is variance information.Gaëtan Gilbert
2018-02-09[error] Replace msg_error by a proper exception.Emilio Jesus Gallego Arias
2018-02-02checker: cleanup projection unfoldingGaëtan Gilbert
2018-02-02checker: remove unused per-constant reduction flags.Gaëtan Gilbert
2018-01-25[checker] Avoid relying on canonical names.Maxime Dénès
2018-01-25[checker] Remove duplicated functionMaxime Dénès
2018-01-25[checker] Better error message for bad recursive treesMaxime Dénès
2018-01-24fix space in coqchk errorRalf Jung
2018-01-20Fix #6618: coqchk fails with "ill-typed term".Pierre-Marie Pédrot
2018-01-14Actually use the strategy information in the checker.Pierre-Marie Pédrot
2018-01-14Store the conversion oracle in constant and inductive definitions.Pierre-Marie Pédrot
2018-01-10Add interfaces for checker and remove dead code.Maxime Dénès
2017-12-30Moving some universe substitution code out of the kernel.Pierre-Marie Pédrot
2017-12-09[lib] Rename Profile to CProfileEmilio Jesus Gallego Arias
2017-12-07Merge PR #6277: Qualified import in coqchkMaxime Dénès
2017-12-07Merge PR #6303: Remove redundant Zcase from the checker.Maxime Dénès
2017-12-05Merge PR #6266: Safe unmarshalling in the checkerMaxime Dénès
2017-12-02Remove redundant Zcase from the checker.Pierre-Marie Pédrot
2017-12-01Documenting the -Q flag of coqchk.Pierre-Marie Pédrot
2017-11-29Forbid implicitly relative names in the checker.Pierre-Marie Pédrot
2017-11-29Mark the -I option in coqchk as deprecated and merge it with -Q.Pierre-Marie Pédrot
2017-11-29Add a -Q option to coqchck.Pierre-Marie Pédrot
2017-11-29Allow to pass physical files to coqchk.Pierre-Marie Pédrot
2017-11-28Adding an interface file for checker/check.ml.Pierre-Marie Pédrot
2017-11-28Use safe demarshalling in the checker.Pierre-Marie Pédrot
2017-11-28Use large arrays in the checker demarshaller.Pierre-Marie Pédrot
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-24When declaring constants/inductives use ContextSet if monomorphic.Gaëtan Gilbert
2017-11-23Truncate strings in votour to 1024 characters.Pierre-Marie Pédrot
2017-11-23Bypass int and string representation in votour when it's incorrect.Pierre-Marie Pédrot
2017-11-23Tail-recursive list traversal in votour.Pierre-Marie Pédrot
2017-11-22Implement a tail-recursive traversal of the object in votour.Pierre-Marie Pédrot
2017-11-13Merge PR #6065: [api] Deprecate all legacy uses of Names in core.Maxime Dénès
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-11-06[feedback] Helper to print feedback messages in the console.Emilio Jesus Gallego Arias
2017-09-25Merge PR #1075: Re-enable checker error messagesMaxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 03:48:05 +0000