index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
dev
/
vm_printers.ml
Commit message (
Expand
)
Author
Age
*
Merge PR #935: Handling evars in the VM
Maxime Dénès
2018-03-04
|
\
|
*
Handling evars in the VM.
Pierre-Marie Pédrot
2018-03-03
*
|
[VM] Unify Const_sorts and Const_type, and remove Vsort.
Maxime Dénès
2018-03-02
|
/
*
Safer VM interfaces
Maxime Dénès
2018-01-26
*
[api] Deprecate all legacy uses of Names in core.
Emilio Jesus Gallego Arias
2017-11-06
*
Fix a bug in cumulativity
Amin Timany
2017-06-16
*
Put all plugins behind an "API".
Matej Kosik
2017-06-07
*
Feedback cleanup
Emilio Jesus Gallego Arias
2016-05-31
*
Refine Gregory Malecha's patch on VM and universe polymorphism.
Maxime Dénès
2015-10-28
*
Adds support for the virtual machine to perform reduction of universe polymor...
Gregory Malecha
2015-10-28
*
Code cleaning in VM (with Benjamin).
Maxime Dénès
2015-10-09
*
adding a missing case for printing zippers.
Gregory Malecha
2015-07-23
*
use a more compact representation of non-constant constructors
Benjamin Gregoire
2015-03-27
*
fix compilation
Benjamin Gregoire
2015-03-26
*
vm_printers: fix compilation
Enrico Tassi
2015-01-15
*
Modulification of identifier
ppedrot
2012-12-14
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
- Ajout d'un cast vm dans la syntaxe : x <: t
bgregoir
2006-07-22
*
Découpage des printers pour ne pas avoir de dépendances en la vm dans les p...
herbelin
2005-01-02