aboutsummaryrefslogtreecommitdiff
path: root/pretyping/typeclasses_errors.ml
AgeCommit message (Expand)Author
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-06-11Fix #10225 (Instance := {} accepts duplicate fields)Gaëtan Gilbert
2019-02-25Fix #9631: Instance: anomaly grounding non evar-free termGaëtan Gilbert
2018-06-12[api] Misctypes removal: miscellaneous aliases.Emilio Jesus Gallego Arias
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-02-14Typeclasses API using EConstr.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-11CLEANUP: kernel/context.ml{,i}Matej Kosik
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-08-22Move UnsatisfiableConstraints to a pretype error.Matthieu Sozeau
2014-03-05Remove some dead-code (thanks to ocaml warnings)Pierre Letouzey
2013-10-06Removing uses of Evar.add in class-related functions.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-02-18Removing Exc_located and using the new exception enrichementppedrot
2012-12-14Modulification of identifierppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evdletouzey
2012-03-02Noise for nothingpboutill
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-05-19Add (almost) compatibility with camlp4, without breaking support for camlp5letouzey
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-11-11Promote evar_defs to evar_map (in Evd)glondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-06-18Fix "unsatisfiable constraints" error messages to include all themsozeau
2009-06-11Use a lazy value for the message in FailError, so that it won't bemsozeau
2009-05-19Remove camlp4-specific exception handlingmsozeau
2009-05-18Minor unification changes:msozeau
2009-02-19On remplace evar_map par evar_defs (seul evar_defs est désormais exporté aspiwack
2008-06-21Code cleanup in typeclasses, remove dead and duplicated code.msozeau
2008-06-17Better typeclass error messages, always giving the full set ofmsozeau
2008-06-11Optionally (and by default) split typeclasses evars into connected msozeau
2008-05-23- Fix bug #1858, Hint Unfold calling the wrong locate function.msozeau
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2008-03-28Improve error handling and messages for typeclasses. msozeau
2008-03-27Various fixes on typeclasses:msozeau
2008-03-19Do another pass on the typeclasses code. Correct globalization of classmsozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:59:57 +0000