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.ml
Commit message (
Expand
)
Author
Age
*
Minor cleanup concerning Mod_subst.MBImap
letouzey
2013-04-02
*
Restrict (try...with...) to avoid catching critical exn (part 2)
letouzey
2013-03-12
*
Names: shortcuts for building {kn, constant, mind} with empty sections
letouzey
2013-02-26
*
Names: Modularize constant and mutual_inductive
letouzey
2013-02-26
*
Mod_subst: misc reformulations
letouzey
2013-02-26
*
Mod_subst: an extra assert
letouzey
2013-02-19
*
Mod_subst: improve sharing during kn substitutions
letouzey
2013-02-18
*
Slightly improving some debugging printing and error message for modules.
herbelin
2013-01-27
*
Modulification of mod_bound_id
ppedrot
2012-12-18
*
Monomorphization (kernel)
ppedrot
2012-11-22
*
More monomorphizations
ppedrot
2012-11-13
*
Removed many calls to OCaml generic equality. This was done by
ppedrot
2012-10-29
*
Remove some dead code in the vm
letouzey
2012-10-02
*
Fixing ocamldoc errors
ppedrot
2012-09-25
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
This patch removes unused "open" (automatically generated from
regisgia
2012-09-14
*
The new ocaml compiler (4.00) has a lot of very cool warnings,
regisgia
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Noise for nothing
pboutill
2012-03-02
*
Mod_subst: some simplifications, some more significant names to functions, etc
letouzey
2011-10-26
*
Mod_subst: Attempt to fix #2608
letouzey
2011-10-24
*
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
*
Some more simplification in Mod_subst
letouzey
2011-02-23
*
Mod_subt: some more refactoring, substitution is also separated in two tables
letouzey
2011-02-11
*
Mod_subst: split delta_resolver in two tables (mp / kn)
letouzey
2011-02-11
*
A fine-grain control of inlining at functor application via priority levels
letouzey
2011-01-31
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Fix likely semantic typos
glondu
2010-09-15
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Fixing spelling: pr_coma -> pr_comma
herbelin
2010-06-12
*
Added a few informations about file lineages (for the most part in kernel)
herbelin
2010-05-09
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
In function "substitution_prefixed_by" the prefix test on module path
soubiran
2010-04-19
*
cf. 12945
soubiran
2010-04-16
*
Added a lazy evaluation of the composition of module substitutions. It improv...
soubiran
2010-02-04
*
Various bug fix on recent features of the module system:
soubiran
2010-01-19
*
declaremods.ml <--- code factoring
soubiran
2009-12-03
*
First debug... the renaming of librairies was not working and auto/dn were no...
soubiran
2009-10-23
*
This big commit addresses two problems:
soubiran
2009-10-21
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Bug 2050, commit v8.2 11923-11924 ---> trunk
soubiran
2009-02-13
*
correction bug 1839
soubiran
2008-04-25
*
Correction d'un bug sur Import/Export : ces fonctionnalites sont gerees en-de...
soubiran
2008-03-26
*
Correction de bugs relatifs a la compostion des substitutions
soubiran
2008-03-25
*
Ajout des alias de module dans le noyau.
soubiran
2008-03-14
*
Memory optimisation for modules and constrs substitutions.
soubiran
2007-05-30
*
Correction of (PR#1576).
soubiran
2007-05-25
[next]