aboutsummaryrefslogtreecommitdiff
path: root/interp/modintern.ml
AgeCommit message (Expand)Author
2019-09-18[library] Move `Declaremods` to `vernac/`Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2018-11-09Force the user to provide names when generating abstract universe contexts.Pierre-Marie Pédrot
2018-11-09Adding universe names to polymorphic entry instances.Pierre-Marie Pédrot
2018-11-02Remove incorrect is_universe_polymorphism from modinternGaëtan Gilbert
2018-06-18Remove reference name type.Maxime Dénès
2018-06-12[api] Misctypes removal: module_kind to DeclaremodsEmilio Jesus Gallego Arias
2018-05-31[api] Move `Constrexpr` to the `interp` module.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-07Merge PR #6790: Allow universe declarations for [with Definition].Maxime Dénès
2018-03-05Allow universe declarations for [with Definition].Gaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-16Extrude monomorphic universe contexts from with Definition constraints.Pierre-Marie Pédrot
2017-11-24Stop exposing UState.universe_context and its Evd wrapper.Gaëtan Gilbert
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-24[constrexpr] Make patterns use Loc.located for location informationEmilio Jesus Gallego Arias
2016-08-19Unify location handling of error functions.Emilio Jesus Gallego Arias
2016-01-20Update copyright headers.Maxime Dénès
2015-05-27Fix bug #4159Matthieu Sozeau
2015-02-12Univs: fix bug #3978: carry around the universe context used toMatthieu Sozeau
2015-01-12Update headers.Maxime Dénès
2014-09-12Uniformisation of the order of arguments env and sigma.Hugo Herbelin
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-07-17Declaremods: major refactoring, stop duplicating libobjects in modulesletouzey
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-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
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-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-03-02Noise for nothingpboutill
2011-08-30Quick improvement of some error messages related to module applicationherbelin
2011-03-05Moving printing of module typing errors upwards to himsg.ml so as toherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-01-07Include can accept both Module and Module Typeletouzey
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-06-25Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...notin
2008-06-14Correction bug 1878 (utilisation de extend_evar déplacée là où uneherbelin
2008-06-06Enhancements to coqdoc, better globalization of sections and modules.msozeau
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2005-01-13Construct "T with (Definition|Module) id := c" generalized tosacerdot
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:03:29 +0000