index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
checker
/
environ.mli
Age
Commit message (
Expand
)
Author
2018-11-06
[checker] Refactor by sharing code with the kernel
Maxime Dénès
2018-07-24
Projections use index representation
Gaëtan Gilbert
2018-06-17
Getting rid of the const_proj field in the kernel.
Pierre-Marie Pédrot
2018-05-31
Reduce circular dependency constants <-> projections
Gaëtan Gilbert
2018-03-28
[api] Deprecate a couple of aliases that we missed.
Emilio Jesus Gallego Arias
2018-01-20
Fix #6618: coqchk fails with "ill-typed term".
Pierre-Marie Pédrot
2018-01-14
Actually use the strategy information in the checker.
Pierre-Marie Pédrot
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-07-26
Removing template polymorphism for definitions.
Pierre-Marie Pédrot
2017-06-16
Clean up universes of constants and inductives
Amin Timany
2015-10-02
Univs: update checker
Matthieu Sozeau
2015-07-10
Option -type-in-type: added support in checker and making it contaminating
Hugo Herbelin
2015-07-07
Checker: Fix bug #4282
Matthieu Sozeau
2014-05-08
Adapt the checker to polymorphic universes and projections (untested).
Matthieu Sozeau
2014-03-11
vi2vo: universes handling finally fixed
Enrico Tassi
2014-03-05
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2013-04-15
Checker: get rid of code handling section variables
letouzey
2013-04-15
Checker: empty sections hardcoded in cb and mind
letouzey
2013-04-15
Checker: regroup all vo-related types in cic.mli
letouzey
2013-02-19
Dir_path --> DirPath
letouzey
2012-12-14
Modulification of dir_path
ppedrot
2012-12-14
Modulification of identifier
ppedrot
2011-10-26
Checker/subtyping.ml: avoid adding in env a module already there (fix #2609)
letouzey
2010-09-24
Checker: remove some dead code
letouzey
2010-04-29
After the approval of Bruno, here the patch for the checker.
soubiran
2009-10-21
This big commit addresses two problems:
soubiran
2009-03-02
porting r11900 11905 and 11953 to trunk
barras
2008-05-22
fixed dependency problems with the checker
barras