index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
vars.ml
Commit message (
Expand
)
Author
Age
*
CLEANUP: minor readability improvements
Matej Kosik
2016-08-24
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
CLEANUP: Context.{Rel,Named}.Declaration.t
Matej Kosik
2016-02-09
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-11
*
|
About building of substitutions from instances.
Hugo Herbelin
2015-12-05
*
|
Experimenting documentation of the Vars.subst functions.
Hugo Herbelin
2015-12-05
|
/
*
Adds support for the virtual machine to perform reduction of universe polymor...
Gregory Malecha
2015-10-28
*
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-15
*
Update headers.
Maxime Dénès
2015-01-12
*
Move to a representation of universe polymorphic constants using indices for ...
Matthieu Sozeau
2014-08-03
*
Cleanup substitution inside universe instances, only done through subst_fn now,
Matthieu Sozeau
2014-07-21
*
- Fix hashing of levels to get the "right" order in universe contexts etc...
Matthieu Sozeau
2014-06-04
*
Various fixes of universe polymorphism and projections when they're set.
Matthieu Sozeau
2014-05-06
*
- Fix comparison of universes.
Matthieu Sozeau
2014-05-06
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove some dead-code (thanks to ocaml warnings)
Pierre Letouzey
2014-03-05
*
Optimization in kernel/vars.ml: directly allocate a fixed-size block in the
Pierre-Marie Pédrot
2014-02-20
*
Less partial applications in Vars, as well as better memory allocation.
ppedrot
2013-11-06
*
Optimizing Vars.replace_vars
ppedrot
2013-10-23
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
Removing useless casts between arrays and lists.
ppedrot
2013-08-04
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29