aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Fixing a bug in the native compiler, introduced by r16363, leading to undefinedGravatar mdenes2013-07-06
* comments in mliGravatar pboutill2013-05-30
* Delayed the computation of parameters in sort polymorphism ofGravatar herbelin2013-05-14
* Replacing Id.check with Id.is_valid, as its sole use was underGravatar ppedrot2013-05-14
* Removing Gmap from Extraction pluginGravatar ppedrot2013-05-12
* Use definition_entry to declare local definitionsGravatar gareuselesinge2013-05-09
* States: frozen states can hold closuresGravatar gareuselesinge2013-05-06
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Minor simplifications in Declaremods and Safe_typingGravatar letouzey2013-04-15
* Checker: regroup all vo-related types in cic.mliGravatar letouzey2013-04-15
* Removing two Pervasives.compare from Term.Gravatar ppedrot2013-04-03
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* Minor cleanup concerning Mod_subst.MBImapGravatar letouzey2013-04-02
* Safe_typing+Libary: use some arrays instead of lists in vo structuresGravatar letouzey2013-03-28
* Safe_library : a record type for compiled_library instead of large tupleGravatar letouzey2013-03-28
* Native compiler: hash-consing of generated code and values.Gravatar mdenes2013-03-25
* Native compiler: Inlined constants are now compiled, fixing a bug reported byGravatar mdenes2013-03-25
* Comments in mliGravatar pboutill2013-03-25
* Minor code cleaning in CArray / CList.Gravatar ppedrot2013-03-23
* Robust display of NotConvertibleTypeField errors (fix #3008, #2995)Gravatar letouzey2013-03-21
* Restrict (try...with...) to avoid catching critical exn (part 8)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 5)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 2)Gravatar letouzey2013-03-12
* Restrict (try...with...) to avoid catching critical exn (part 1)Gravatar letouzey2013-03-12
* A version of Univ.check_eq with no anomaly for Evd.set_eq_sortGravatar letouzey2013-03-12
* Term.dest* functions now raise specific DestKO exn instead of Invalid_argumentGravatar letouzey2013-03-12
* invalid_arg instead of raise (Invalid_argement ...)Gravatar letouzey2013-03-12
* More monomorphization.Gravatar ppedrot2013-03-05
* More informative error when a global reference is used in a context ofGravatar herbelin2013-02-28
* Minor cleanup around Term_typingGravatar letouzey2013-02-27
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
* Names: Modularize constant and mutual_inductiveGravatar letouzey2013-02-26
* Mod_subst: misc reformulationsGravatar letouzey2013-02-26
* Fixing bug #2466Gravatar ppedrot2013-02-24
* Reduced the noise level when dynlinking in bytecode mode or whenGravatar mdenes2013-02-24
* Names: con_modpath and con_label access back the user kn partGravatar letouzey2013-02-21
* avoid (Int.equal (cmp ...) 0) when a boolean equality existsGravatar letouzey2013-02-19
* Dir_path --> DirPathGravatar letouzey2013-02-19
* module_path --> ModPath.t, kernel_name --> KerName.tGravatar letouzey2013-02-19
* Mod_subst: an extra assertGravatar letouzey2013-02-19
* Names: revised representation of constants and mutual_inductiveGravatar letouzey2013-02-19
* Mod_subst: improve sharing during kn substitutionsGravatar letouzey2013-02-18
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
* Fixing bug in native compiler with let patterns in fixpoint definitions.Gravatar mdenes2013-02-11
* Actually adding backtrace handling.Gravatar ppedrot2013-01-28
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28