aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/modintern.ml
Commit message (Expand)AuthorAge
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
* Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* Univs: fix bug #3978: carry around the universe context used toGravatar Matthieu Sozeau2015-02-12
* Update headers.Gravatar Maxime Dénès2015-01-12
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Declaremods: major refactoring, stop duplicating libobjects in modulesGravatar letouzey2013-07-17
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Quick improvement of some error messages related to module applicationGravatar herbelin2011-08-30
* Moving printing of module typing errors upwards to himsg.ml so as toGravatar herbelin2011-03-05
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* Correction bug 1878 (utilisation de extend_evar déplacée là où uneGravatar herbelin2008-06-14
* Enhancements to coqdoc, better globalization of sections and modules.Gravatar msozeau2008-06-06
* Beaoucoup de changements dans la representation interne des modules.Gravatar soubiran2008-02-01
* Construct "T with (Definition|Module) id := c" generalized toGravatar sacerdot2005-01-13
* Nouvelle en-têteGravatar herbelin2004-07-16
* meilleure presentation des commentaires du traducteurGravatar barras2004-01-02
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14