aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* Modulification of LabelGravatar ppedrot2012-12-18
* Fixing ocalmdoc commentGravatar ppedrot2012-12-14
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Moving hcons_string to String namespace.Gravatar ppedrot2012-12-14
* Renamed Option.Misc.compare to the more uniform Option.equal.Gravatar ppedrot2012-12-13
* * Implementing the "union by rank" optimisation in univ.mlGravatar pboutill2012-12-10
* Small optimization in Closure: replaced an index list with an array.Gravatar ppedrot2012-12-08
* Fixing a comment.Gravatar herbelin2012-12-04
* Kernel/closure: add eta red_kindGravatar pboutill2012-11-28
* Removed some FIXME related to equality on universes.Gravatar ppedrot2012-11-26
* Small cleaning of interface in UnivGravatar ppedrot2012-11-26
* More equality functionsGravatar ppedrot2012-11-25
* Monomorphization (kernel)Gravatar ppedrot2012-11-22
* More monomorphizationsGravatar ppedrot2012-11-13
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Removing another bunch of generic equalitiesGravatar ppedrot2012-11-08
* Removed many calls to OCaml generic equality. This was done byGravatar ppedrot2012-10-29
* Moved Entries module back to kernelGravatar ppedrot2012-10-26
* Cleared a purely declarative .ml file and moved its interface to intf/Gravatar ppedrot2012-10-23
* univ inconsistency error message gives evidence of a cycleGravatar barras2012-10-17
* Remove some dead code in the vmGravatar letouzey2012-10-02
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Default hashconsing of identifiers.Gravatar ppedrot2012-09-27
* Reusing the Hashset data structure in Hashcons. Hopefully, this shouldGravatar ppedrot2012-09-26
* Incorrect commentGravatar msozeau2012-09-26
* Cleaning, renaming obscure functions and documenting in Hashcons.Gravatar ppedrot2012-09-26
* Fixing ocamldoc errorsGravatar ppedrot2012-09-25
* More cleanup of Util: utf8 aspects moved to a new file unicode.mlGravatar letouzey2012-09-18
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* kernel/Term:Gravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* fast bitwise operations (lor,land,lxor) on int31 and BigNGravatar letouzey2012-08-11
* Updating headers.Gravatar herbelin2012-08-08
* Fixing bug #2817 (occur check was not done up to instantiation ofGravatar herbelin2012-06-20
* Proof using: nested sections bugfixGravatar gareuselesinge2012-06-18
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Adding newline after warning and restoring distinction betweenGravatar herbelin2012-04-15
* Shortcuts and optimizations of comparisonsGravatar xclerc2012-04-05
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
* Univ: enforce_leq instead of enforce_geq for more uniformityGravatar letouzey2012-03-22
* Univ: switch the order of int and dir_path in UniverseLevel.LevelGravatar letouzey2012-03-22
* Reorganizing the structure of evarutil.ml (only restructuration, noGravatar herbelin2012-03-20
* Final part of moving Program code inside the main code. Adapted add_definitio...Gravatar msozeau2012-03-14