index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
kernel
/
vars.mli
Age
Commit message (
Expand
)
Author
2020-03-28
Remove a useless reversed variant in Vars.
Pierre-Marie Pédrot
2020-03-18
Update headers in the whole code base.
Théo Zimmermann
2019-06-17
Update ml-style headers to new year.
Théo Zimmermann
2018-12-05
Fix mod_subst wrt universe polymorphism
Gaëtan Gilbert
2018-10-16
{Univops -> Vars}.universes_of_constr
Gaëtan Gilbert
2018-06-27
Swapping Context and Constr: defining declarations on constr in Constr.
Hugo Herbelin
2018-03-05
Merge PR #6855: Update headers following #6543.
Maxime Dénès
2018-03-03
Handling evars in the VM.
Pierre-Marie Pédrot
2018-02-27
Update headers following #6543.
Théo Zimmermann
2017-12-30
Moving some universe substitution code out of the kernel.
Pierre-Marie Pédrot
2017-11-06
[api] Move structures deprecated in the API to the core.
Emilio Jesus Gallego Arias
2017-11-06
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-05-01
More consistent writing of de Bruijn.
Théo Zimmermann
2017-02-14
Merge branch 'master'.
Pierre-Marie Pédrot
2016-12-22
Fixing injection in the presence of let-in in constructors.
Hugo Herbelin
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2016-01-13
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-11
CLEANUP: kernel/context.ml{,i}
Matej Kosik
2016-01-07
Fix a misleading comment for substn_vars
Matthieu Sozeau
2015-12-05
About building of substitutions from instances.
Hugo Herbelin
2015-12-05
Experimenting documentation of the Vars.subst functions.
Hugo Herbelin
2015-10-28
Adds support for the virtual machine to perform reduction of universe polymor...
Gregory Malecha
2015-01-15
Correct restriction of vm_compute when handling universe polymorphic
Matthieu Sozeau
2015-01-12
Update headers.
Maxime Dénès
2014-08-03
Move to a representation of universe polymorphic constants using indices for ...
Matthieu Sozeau
2014-07-21
Cleanup substitution inside universe instances, only done through subst_fn now,
Matthieu Sozeau
2014-06-04
- Fix hashing of levels to get the "right" order in universe contexts etc...
Matthieu Sozeau
2014-05-06
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-04-23
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2013-12-16
A few fixes to the build system (mostly for ocamlbuild)
Pierre Letouzey
2013-05-30
comments in mli
pboutill
2013-04-29
Merging Context and Sign.
ppedrot
2013-04-29
Splitting Term into five unrelated interfaces:
ppedrot
