index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
kernel
Commit message (
Expand
)
Author
Age
*
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
*
compatibility <3.12 (Map.exists Map.singleton)
pboutill
2011-02-11
*
A fine-grain control of inlining at functor application via priority levels
letouzey
2011-01-31
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
Make simpl use the proper constant when folding (mutual) fixpoints
letouzey
2011-01-27
*
Rewrite sort_universes to minimize the number of universes
glondu
2011-01-25
*
In univ.ml, put universe_level primitives in its their own sub-module
glondu
2011-01-11
*
Add "Print Sorted Universes"
glondu
2011-01-11
*
More coherent comment ordering
glondu
2011-01-11
*
Fixing bug #2454: inversion predicate strategy for inferring the type
herbelin
2010-12-19
*
Univ: try to avoid a few lookup in the universe graph
letouzey
2010-12-18
*
Univ.constraints made fully abstract instead of being a Set of abstract stuff
letouzey
2010-12-18
*
Revert last commit 13723 on Univ : minor gains and more complex code
letouzey
2010-12-18
*
Univ: an attempt to lazily compact chains of Equiv in a functionnal way
letouzey
2010-12-17
*
Univ: two improvements (speed + space)
letouzey
2010-12-16
*
* Kernel/Term:
regisgia
2010-12-01
*
* Kernel/Term
regisgia
2010-12-01
*
* Kernel/Term
regisgia
2010-12-01
*
Minor fixes from Gregory Malecha. A typo fixed and a better (located)
msozeau
2010-11-15
*
Correction bug 2427
soubiran
2010-11-03
*
Remove suspiciously named "implicit" stuff from Term
glondu
2010-11-03
*
In Univ, unify order_request and constraint_type
glondu
2010-11-03
*
More generic Univ.dump_universes
glondu
2010-11-02
*
Reintroduce kind_of_type (used by Presburger contrib)
glondu
2010-10-05
*
Forgotten lifts in eta-expansion
glondu
2010-10-04
*
Fixing printing of module_path names (was using a debugging
herbelin
2010-10-03
*
Remove kind_of_type, kind_of_term2 (dead code)
glondu
2010-09-28
*
Partial review of removed dead code (r13460)
herbelin
2010-09-24
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Fix inconsistency in Prop/Set conversion check
glondu
2010-09-23
*
Added eta-expansion in kernel, type inference and tactic unification,
herbelin
2010-09-20
*
Sharing is not anymore broken by traverse_module.
soubiran
2010-09-15
*
Fix likely semantic typos
glondu
2010-09-15
*
* kernel/Safe_typing.LightenLibrary:
regisgia
2010-08-27
*
* (checker|kernel)/Safe_typing:
regisgia
2010-08-27
*
* (checker|kernel)/Safe_typing:
regisgia
2010-08-27
*
* checker/SafeTyping kernel/SafeTyping:
regisgia
2010-08-27
*
* Improve documentation of LightenLibrary.
regisgia
2010-08-27
*
* (checker|kernel)/Safe_typing: New LightenLibrary.
regisgia
2010-08-27
*
better fix to bug #2319: types are compiled in the env of the bodies
barras
2010-07-30
*
kernel conversion and reduction do not raise assert failure on ill-typed term...
barras
2010-07-29
*
fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...
barras
2010-07-29
*
ported r13340 to trunk
barras
2010-07-28
*
fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodies
barras
2010-07-28
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
fixed (serious) bug #2353: non-recursive parameters of nested inductive types...
barras
2010-07-16
*
removed a potentially dangerous try ... with _ -> ...
barras
2010-07-16
*
Mod_typing: fix the content of the typ_expr_alg field
letouzey
2010-07-07
*
Names: remove obsolete mod_self_id
letouzey
2010-06-23
[next]