aboutsummaryrefslogtreecommitdiff
path: root/vernac/himsg.ml
AgeCommit message (Expand)Author
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
2018-10-28[error printing] Fix improper grounding of open terms in printing.Emilio Jesus Gallego Arias
2018-10-26[typeclasses] functionalize typeclass evar handlingMatthieu Sozeau
2018-10-26Cleanup evar_extra: remove evar_info's store and add maps to evar_mapMatthieu Sozeau
2018-09-28Functionalizing calls to the environment in Himsg.Hugo Herbelin
2018-09-27Merge PR #8475: Centralize the reliance on abstract universe context internalsGaëtan Gilbert
2018-09-21Removing calls to AUContext.instance.Pierre-Marie Pédrot
2018-09-19Fix Numeral Notations (2/4 - exceptions, usr_err)Jason Gross
2018-09-03Merge PR #891: Check universes are declaredGaëtan Gilbert
2018-07-26Merge PR #7786: In "redundant clause" pattern-matching error, show also the p...Pierre-Marie Pédrot
2018-07-25In "redundant clause" pattern-matching error, show also the pattern (#7777).Hugo Herbelin
2018-07-25kernel: missing check that all universes are declared.Matthieu Sozeau
2018-07-25Remove himsg.pr_puniverses, use @{} for universe printing in errorsMaxime Dénès
2018-07-17Change QuestionMark for better record field missing error message.Siddharth Bhat
2018-06-22Remove hack skipping comparison of algebraic universes in subtyping.Gaëtan Gilbert
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-23Collecting Array.smart_* functions into a module Array.Smart.Hugo Herbelin
2018-05-17Split off Universes functions dealing with names.Gaëtan Gilbert
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-24Slightly refining some error messages about unresolvable evars.Hugo Herbelin
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-09Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec valuesMaxime Dénès
2018-03-08Fix SR breakage due to allowing fixpoints on non-rec valuesMatthieu Sozeau
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-02Reductionops.nf_* now take an environment.Gaëtan Gilbert
2017-11-22[api] Deprecate Term destructors, move to ConstrEmilio Jesus Gallego Arias
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-11-13[api] Another large deprecation, `Nameops`Emilio Jesus Gallego Arias
2017-11-06[api] Deprecate all legacy uses of Names in core.Emilio Jesus Gallego Arias
2017-09-22Himsg: Dropping nf_evars made obsolete by EConstr.Hugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 13:47:46 +0000