aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 5)letouzey
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 2)letouzey
2013-03-12Restrict (try...with...) to avoid catching critical exn (part 1)letouzey
2013-03-12A version of Univ.check_eq with no anomaly for Evd.set_eq_sortletouzey
2013-03-12Term.dest* functions now raise specific DestKO exn instead of Invalid_argumentletouzey
2013-03-12invalid_arg instead of raise (Invalid_argement ...)letouzey
2013-03-05More monomorphization.ppedrot
2013-02-28More informative error when a global reference is used in a context ofherbelin
2013-02-27Minor cleanup around Term_typingletouzey
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
2013-02-26Names: Modularize constant and mutual_inductiveletouzey
2013-02-26Mod_subst: misc reformulationsletouzey
2013-02-24Fixing bug #2466ppedrot
2013-02-24Reduced the noise level when dynlinking in bytecode mode or whenmdenes
2013-02-21Names: con_modpath and con_label access back the user kn partletouzey
2013-02-19avoid (Int.equal (cmp ...) 0) when a boolean equality existsletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-19module_path --> ModPath.t, kernel_name --> KerName.tletouzey
2013-02-19Mod_subst: an extra assertletouzey
2013-02-19Names: revised representation of constants and mutual_inductiveletouzey
2013-02-18Mod_subst: improve sharing during kn substitutionsletouzey
2013-02-18use List.rev_map whenever possibleletouzey
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2013-02-11Fixing bug in native compiler with let patterns in fixpoint definitions.mdenes
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-28native_compute: Fixed dependencies compilation order.mdenes
2013-01-27Slightly improving some debugging printing and error message for modules.herbelin
2013-01-24Native compiler: warnings were not turned off for OCaml 3.11mdenes
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2013-01-06* Kernel/Terms:regisgia
2012-12-19Array.create is deprecatedpboutill
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of mod_bound_idppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Fixing ocalmdoc commentppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moving hcons_string to String namespace.ppedrot
2012-12-13Renamed Option.Misc.compare to the more uniform Option.equal.ppedrot
2012-12-10* Implementing the "union by rank" optimisation in univ.mlpboutill
2012-12-08Small optimization in Closure: replaced an index list with an array.ppedrot
2012-12-04Fixing a comment.herbelin
2012-11-28Kernel/closure: add eta red_kindpboutill
2012-11-26Removed some FIXME related to equality on universes.ppedrot
2012-11-26Small cleaning of interface in Univppedrot
2012-11-25More equality functionsppedrot
2012-11-22Monomorphization (kernel)ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 22:16:06 +0000