aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Expand)AuthorAge
* 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
* Fixing vm_compute bug #2729 (function used to decompose constructorsGravatar herbelin2012-03-13
* Univ: avoid recording dummy universe constraints u<=u or u=uGravatar letouzey2012-03-12
* Noise for nothingGravatar pboutill2012-03-02
* Univ: a univ_depends function to avoid a hack in InductiveopsGravatar letouzey2012-03-01
* Univ: a better Constraint.compareGravatar letouzey2012-03-01
* Univ: a faster is_leq test used when possibleGravatar letouzey2012-02-29
* Univ: correct compare_neq (fix #2703)Gravatar letouzey2012-02-27
* Proof using ...Gravatar gareuselesinge2011-12-12
* Term: properly ignore Casts between Apps in constr_ordGravatar puech2011-11-29
* Term: useless conversion to list in constr_ord deletedGravatar puech2011-11-29
* Term: Fix hash_constr behavior for Cast lnterleaved in application spines.Gravatar puech2011-11-28
* TypoGravatar herbelin2011-11-21
* When checking for emptiness, use Foo.is_empty instead of (=) Foo.emptyGravatar letouzey2011-10-26
* Environ.set_universes is dead codeGravatar letouzey2011-10-26
* Mod_subst: some simplifications, some more significant names to functions, etcGravatar letouzey2011-10-26
* First attempt at making Print Assumption compatible with opaque modules (fix ...Gravatar letouzey2011-10-25
* Mod_subst: Attempt to fix #2608Gravatar letouzey2011-10-24
* Safe_typing: adding a inductive block adds many labels (fix #2603)Gravatar letouzey2011-10-11
* Names : check of labels, cleanup, nicer debug display of kn and constantGravatar letouzey2011-10-11
* Mod_subst: an unused functionGravatar letouzey2011-10-11
* More on r14536 (an unused pattern-matching remained in the commit).Gravatar herbelin2011-10-11