index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
/
mod_subst.mli
Commit message (
Expand
)
Author
Age
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Lazyconstr -> Opaqueproof
Enrico Tassi
2014-02-26
*
Mod_subst: misc reformulations
letouzey
2013-02-26
*
Modulification of mod_bound_id
ppedrot
2012-12-18
*
Updating headers.
herbelin
2012-08-08
*
Mod_subst: some simplifications, some more significant names to functions, etc
letouzey
2011-10-26
*
Mod_subst: an unused function
letouzey
2011-10-11
*
Various simplifications about constant_of_delta and mind_of_delta
letouzey
2011-10-11
*
fixed bug 2580. Quick fix: copy emitcodes before patching it
barras
2011-08-01
*
Mod_subst: improving sharing of subst_mps
letouzey
2011-02-24
*
A fine-grain control of inlining at functor application via priority levels
letouzey
2011-01-31
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
correction bug 1839
soubiran
2008-04-25
*
Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees en-de...
soubiran
2008-03-26
*
Ajout des alias de module dans le noyau.
soubiran
2008-03-14
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
HUGE COMMIT
sacerdot
2005-01-03
*
* added subst_evaluable_reference
sacerdot
2004-12-07
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16