aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Expand)Author
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
2012-11-13More monomorphizationsppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-11-08Removing another bunch of generic equalitiesppedrot
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
2012-10-26Moved Entries module back to kernelppedrot
2012-10-23Cleared a purely declarative .ml file and moved its interface to intf/ppedrot
2012-10-17univ inconsistency error message gives evidence of a cyclebarras
2012-10-02Remove some dead code in the vmletouzey
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-27Default hashconsing of identifiers.ppedrot
2012-09-26Reusing the Hashset data structure in Hashcons. Hopefully, this shouldppedrot
2012-09-26Incorrect commentmsozeau
2012-09-26Cleaning, renaming obscure functions and documenting in Hashcons.ppedrot
2012-09-25Fixing ocamldoc errorsppedrot
2012-09-18More cleanup of Util: utf8 aspects moved to a new file unicode.mlletouzey
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-09-14kernel/Term:regisgia
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-11fast bitwise operations (lor,land,lxor) on int31 and BigNletouzey
2012-08-08Updating headers.herbelin
2012-06-20Fixing bug #2817 (occur check was not done up to instantiation ofherbelin
2012-06-18Proof using: nested sections bugfixgareuselesinge
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-30More uniformisation in Pp.warn functions.ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-04-15Adding newline after warning and restoring distinction betweenherbelin
2012-04-05Shortcuts and optimizations of comparisonsxclerc
2012-03-26Module names and constant/inductive names are now in two separate namespacesletouzey
2012-03-22Univ: enforce_leq instead of enforce_geq for more uniformityletouzey
2012-03-22Univ: switch the order of int and dir_path in UniverseLevel.Levelletouzey
2012-03-20Reorganizing the structure of evarutil.ml (only restructuration, noherbelin
2012-03-14Final part of moving Program code inside the main code. Adapted add_definitio...msozeau
2012-03-13Fixing vm_compute bug #2729 (function used to decompose constructorsherbelin
2012-03-12Univ: avoid recording dummy universe constraints u<=u or u=uletouzey
2012-03-02Noise for nothingpboutill
2012-03-01Univ: a univ_depends function to avoid a hack in Inductiveopsletouzey
2012-03-01Univ: a better Constraint.compareletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:41:34 +0000