aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/modops.ml
Commit message (Expand)AuthorAge
* Statically enforcing that module types have no retroknowledge.Gravatar Pierre-Marie Pédrot2017-08-29
* Separating the module_type and module_body types by using a type parameter.Gravatar Pierre-Marie Pédrot2017-08-29
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Checker: avoid using obsolete names from NamesGravatar Pierre Letouzey2016-05-31
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* Univs: update checkerGravatar Matthieu Sozeau2015-10-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Declarations.mli refactoring: module_type_body = module_bodyGravatar Pierre Letouzey2015-01-11
* Adapt the checker to polymorphic universes and projections (untested).Gravatar Matthieu Sozeau2014-05-08
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Checker: regroup all vo-related types in cic.mliGravatar letouzey2013-04-15
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* still some more dead code removalGravatar letouzey2012-10-06
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Noise for nothingGravatar pboutill2012-03-02
* Modops: the strengthening functions can work without any env argumentGravatar letouzey2011-05-17
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Checker: remove some dead codeGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* After the approval of Bruno, here the patch for the checker.Gravatar soubiran2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* added validation of delta_resolver (which seem to have an impact on typing)Gravatar barras2010-02-19
* [checker] fixed vo validation problems, module incompatibilities remainGravatar barras2010-02-19
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* porting r11900 11905 and 11953 to trunkGravatar barras2009-03-02
* Report des commits 11417 et 11437 de la v8.2Gravatar soubiran2008-10-15
* fixed bug with aliasesGravatar barras2008-05-07
* added the .vo checker (with independent Makefile)Gravatar barras2008-04-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-23 14:17:45 +0000