aboutsummaryrefslogtreecommitdiff
path: root/vernac/himsg.ml
AgeCommit message (Expand)Author
2021-03-24Mention label name in signature mismatch error when constant expectedGaëtan Gilbert
2020-12-09Using self-documenting argument names in two exceptions of cases.ml.Hugo Herbelin
2020-12-09Fixing support for argument scopes and let-ins while interning cases patterns.Hugo Herbelin
2020-11-26Merge PR #13415: Separate interning and pretyping of universescoqbot-app[bot]
2020-11-25Separate interning and pretyping of universesGaëtan Gilbert
2020-11-24Add a new evar source to refer to evars which are types of evars.Hugo Herbelin
2020-11-16Improve bad variance error message: mention expected and actual variancesGaëtan Gilbert
2020-11-16Infrastructure for cumulative inductive syntax (no grammar extension yet)Gaëtan Gilbert
2020-10-21Introduce an Ind module in the Names API.Pierre-Marie Pédrot
2020-10-12Catch more errors in Unification.abstract_list_allGaëtan Gilbert
2020-10-08Dropping the misleading int argument of Pp.h.Hugo Herbelin
2020-10-01Merge PR #13108: Getting rid of temerarious EConstr.to_constr in Himsgcoqbot-app[bot]
2020-09-28Getting rid of temerarious EConstr.to_constr in Himsg.Hugo Herbelin
2020-09-28More precise information when unification fails because of incompatible candi...Hugo Herbelin
2020-07-21Turn various anomalies into regular errors in primitive declaration pathGaëtan Gilbert
2020-07-01UIP in SPropGaëtan Gilbert
2020-06-30Merge PR #12599: Remove the Refiner moduleEmilio Jesus Gallego Arias
2020-06-29Move the FailError exception from Refiner to Tacticals.Pierre-Marie Pédrot
2020-06-25Generate names for anonymous polymorphic universesGaëtan Gilbert
2020-05-12Remove legacy Refiner error constructors.Pierre-Marie Pédrot
2020-05-12Do not use Unsafe.to_constr for old refiner conclusion.Pierre-Marie Pédrot
2020-04-27Improve the Allow SProp error message.Théo Zimmermann
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-02-24[exn] Forbid raising in exn printers, make them return Pp.t optionEmilio Jesus Gallego Arias
2020-02-20Unconditionally print explanation for universe inconsistenciesGaëtan Gilbert
2020-02-12ReferenceVariables error contains a globref instead of a constrGaëtan Gilbert
2020-01-29Nicer kernel universe error for inductivesGaëtan Gilbert
2020-01-16[mltop] Remove error handling hacks in favor of default methods.Emilio Jesus Gallego Arias
2019-12-31Merge PR #11338: Remove uses of Global in Evd API.Gaëtan Gilbert
2019-12-26Remove uses of Global in Evd API.Pierre-Marie Pédrot
2019-12-23Fixes a small bug exposing an _ANONYMOUS_REL in a unification error message.Hugo Herbelin
2019-12-06Moving the diversity of constr printers to a label style.Hugo Herbelin
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-09-18[declaremods] Remove abstraction layer over module interpretation.Emilio Jesus Gallego Arias
2019-07-07[error] Remove special error printing pre-processingEmilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-11Fix #10225 (Instance := {} accepts duplicate fields)Gaëtan Gilbert
2019-05-27mind_kelim is the highest allowed sort instead of a listGaëtan Gilbert
2019-05-10[api] Remove 8.10 deprecations.Emilio Jesus Gallego Arias
2019-05-07Show diffs in error messages only if Diffs is enabledJim Fehrle
2019-04-10Functionalize env in type classesMaxime Dénès
2019-04-10Improve SProp error message to mention the Allow StrictProp flag.Théo Zimmermann
2019-03-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-03-20Merge PR #8669: Show diffs in some error messagesEmilio Jesus Gallego Arias
2019-03-17Use local universe names when printing universe inconsistencyGaëtan Gilbert
2019-03-14Inductives in SProp, forbid primitive records with only sprop fieldsGaëtan Gilbert
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-03-14Add a non-cumulative impredicative universe SProp.Gaëtan Gilbert
2019-03-13Merge PR #9627: Small retroknowledge/primitive cleanupVincent Laporte
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 08:07:29 +0000