aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Mod_subt: some more refactoring, substitution is also separated in two tablesGravatar letouzey2011-02-11
* Mod_subst: split delta_resolver in two tables (mp / kn)Gravatar letouzey2011-02-11
* compatibility <3.12 (Map.exists Map.singleton)Gravatar pboutill2011-02-11
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Make simpl use the proper constant when folding (mutual) fixpointsGravatar letouzey2011-01-27
* Rewrite sort_universes to minimize the number of universesGravatar glondu2011-01-25
* In univ.ml, put universe_level primitives in its their own sub-moduleGravatar glondu2011-01-11
* Add "Print Sorted Universes"Gravatar glondu2011-01-11
* More coherent comment orderingGravatar glondu2011-01-11
* Fixing bug #2454: inversion predicate strategy for inferring the typeGravatar herbelin2010-12-19
* Univ: try to avoid a few lookup in the universe graphGravatar letouzey2010-12-18
* Univ.constraints made fully abstract instead of being a Set of abstract stuffGravatar letouzey2010-12-18
* Revert last commit 13723 on Univ : minor gains and more complex codeGravatar letouzey2010-12-18
* Univ: an attempt to lazily compact chains of Equiv in a functionnal wayGravatar letouzey2010-12-17
* Univ: two improvements (speed + space)Gravatar letouzey2010-12-16
* * Kernel/Term:Gravatar regisgia2010-12-01
* * Kernel/TermGravatar regisgia2010-12-01
* * Kernel/TermGravatar regisgia2010-12-01
* Minor fixes from Gregory Malecha. A typo fixed and a better (located) Gravatar msozeau2010-11-15
* Correction bug 2427Gravatar soubiran2010-11-03
* Remove suspiciously named "implicit" stuff from TermGravatar glondu2010-11-03
* In Univ, unify order_request and constraint_typeGravatar glondu2010-11-03
* More generic Univ.dump_universesGravatar glondu2010-11-02
* Reintroduce kind_of_type (used by Presburger contrib)Gravatar glondu2010-10-05
* Forgotten lifts in eta-expansionGravatar glondu2010-10-04
* Fixing printing of module_path names (was using a debuggingGravatar herbelin2010-10-03
* Remove kind_of_type, kind_of_term2 (dead code)Gravatar glondu2010-09-28
* Partial review of removed dead code (r13460)Gravatar herbelin2010-09-24
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Fix inconsistency in Prop/Set conversion checkGravatar glondu2010-09-23
* Added eta-expansion in kernel, type inference and tactic unification,Gravatar herbelin2010-09-20
* Sharing is not anymore broken by traverse_module.Gravatar soubiran2010-09-15
* Fix likely semantic typosGravatar glondu2010-09-15
* * kernel/Safe_typing.LightenLibrary:Gravatar regisgia2010-08-27
* * (checker|kernel)/Safe_typing:Gravatar regisgia2010-08-27
* * (checker|kernel)/Safe_typing:Gravatar regisgia2010-08-27
* * checker/SafeTyping kernel/SafeTyping:Gravatar regisgia2010-08-27
* * Improve documentation of LightenLibrary.Gravatar regisgia2010-08-27
* * (checker|kernel)/Safe_typing: New LightenLibrary.Gravatar regisgia2010-08-27
* better fix to bug #2319: types are compiled in the env of the bodiesGravatar barras2010-07-30
* kernel conversion and reduction do not raise assert failure on ill-typed term...Gravatar barras2010-07-29
* fixed bug #2105 (compilation of free de Bruijn) and missing lift of predicate...Gravatar barras2010-07-29
* ported r13340 to trunkGravatar barras2010-07-28
* fixed bug #2139: compiled cofix loops, missing offset to evaluate cofix bodiesGravatar barras2010-07-28
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* fixed (serious) bug #2353: non-recursive parameters of nested inductive types...Gravatar barras2010-07-16
* removed a potentially dangerous try ... with _ -> ...Gravatar barras2010-07-16
* Mod_typing: fix the content of the typ_expr_alg fieldGravatar letouzey2010-07-07
* Names: remove obsolete mod_self_idGravatar letouzey2010-06-23