aboutsummaryrefslogtreecommitdiff
path: root/toplevel/class.ml
AgeCommit message (Expand)Author
2017-02-15[stm] Break stm/toplevel dependency loop.Emilio Jesus Gallego Arias
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
2016-09-20Stylistic improvements in intf/decl_kinds.mli.Maxime Dénès
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
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-12-05Moving extended_rel_vect/extended_rel_list to the kernel.Hugo Herbelin
2015-10-28Univs: local names handling.Matthieu Sozeau
2015-10-05Univs: fix handling of evar_map in identity coercion construction.Matthieu Sozeau
2015-05-13Safer typing primitives.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-12-09Switch the few remaining iso-latin-1 files to utf8Pierre Letouzey
2014-07-29Fix bug #3453, not recognizing primitive projections in Coercion declarations.Matthieu Sozeau
2014-06-17Adapt coercion code to work with projections as target classes.Matthieu Sozeau
2014-06-08Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofPierre-Marie Pédrot
2014-06-08Enforce a correct exception handling in declaration_hooksEnrico Tassi
2014-06-04Collecting in Namegen those conventional default names that are used in diffe...Hugo Herbelin
2014-05-06Rework handling of universes on top of the STM, allowing for delayedMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-10-18declaration_hooks use Ephemerongareuselesinge
2013-08-08get rid of closures in global/proof stategareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of identifierppedrot
2012-11-26Monomorphization (toplevel)ppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
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-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-30More uniformisation in Pp.warn functions.ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Decl_kinds becomes a pure mli file, remaining ops in new file kindops.mlletouzey
2012-04-05Relax uniform inheritance conditiongareuselesinge
2012-03-02Noise for nothingpboutill
2011-12-12Proof using ...gareuselesinge
2011-07-29Class: generic equality on constr replaced by destructorspuech
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-02-11An automatic substitution of scope at functor applicationletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:21:05 +0000