aboutsummaryrefslogtreecommitdiff
path: root/vernac/himsg.ml
AgeCommit message (Expand)Author
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
2019-03-11Nicer error for bad primitive types (through type_errors etc)Gaëtan Gilbert
2019-02-28Show diffs in error messages if color is enabledJim Fehrle
2019-02-25Fix #9631: Instance: anomaly grounding non evar-free termGaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2019-02-11Fix #9527: unknown evar in nonterminating [fix] error.Gaëtan Gilbert
2019-02-04Merge PR #9144: Fixes #4633: clearer message unknown existentialPierre-Marie Pédrot
2019-01-21Refactor typechecking of inductive typesGaëtan Gilbert
2019-01-21Move inductive_error to Type_errorsGaëtan Gilbert
2019-01-06Reworking error message for unresolved evar subterm of another evar.Hugo Herbelin
2019-01-06Fixes #4633: more explicit error message when referring to a generated evar.Hugo Herbelin
2018-12-12Merge PR #8965: Add `String Notation` vernacular like `Numeral Notation`Hugo Herbelin
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-11-28Factor out common code in numeral/string notationsJason Gross
2018-11-28Add `String Notation` vernacular like `Numeral Notation`Jason Gross
2018-11-16Print universe names in subtyping error instead of Var(x).Gaëtan Gilbert
2018-11-16Print full binders in subtyping incompatible polymorphism error.Gaëtan Gilbert
2018-11-06Move debug term printer to kernelMaxime Dénès
2018-11-02Merge PR #8834: [error printing] Fix improper grounding of open terms in prin...Hugo Herbelin
2018-10-30Generalizing the various evar_map printers in Termops over an environment.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 15:19:06 +0000