aboutsummaryrefslogtreecommitdiff
path: root/checker
AgeCommit message (Expand)Author
2018-06-07Fix the checker by merely adapting the data structure.Pierre-Marie Pédrot
2018-06-04Merge PR #7552: Fix #7539: Checker does not properly handle negative coinduct...Matthieu Sozeau
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
2018-05-25Merge PR #7325: Fix #7323: coqchk puts polymorphic univs of inductive in glob...Pierre-Marie Pédrot
2018-05-24Merge PR #7177: Unifying names of "smart" combinators + adding combinators in...Pierre-Marie Pédrot
2018-05-24Fix #7323: coqchk puts polymorphic univs of inductive in global envGaëtan Gilbert
2018-05-24Merge PR #7328: Fix #7327: coqchk subtyping of polymorphic constantsPierre-Marie Pédrot
2018-05-24Merge PR #7317: Fix #6798: coqchk ignores ugraph when comparing constant inst...Pierre-Marie Pédrot
2018-05-23Moving Rtree.smart_map into Rtree.Smart.map.Hugo Herbelin
2018-05-23Moving Option.smart_map to Option.Smart.map.Hugo Herbelin
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-18Fix #7539: Checker does not properly handle negative coinductive types.Pierre-Marie Pédrot
2018-05-13Infrastructure for ocamldebug on the checkerGaëtan Gilbert
2018-04-23Fix #7327: coqchk subtyping of polymorphic constantsGaëtan Gilbert
2018-04-20Fix #6798: coqchk ignores ugraph when comparing constant instancesGaëtan Gilbert
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-03-09Merge PR #6800: [checker] Printer cleanup.Maxime Dénès
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 23:54:32 +0000