aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2013-03-13Modules and ppvernac, sequel of Enrico's commit 16261letouzey
2013-03-13Declaremods: a few syntactic improvementsletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 6)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 1)letouzey
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-26Names: shortcuts for building {kn, constant, mind} with empty sectionsletouzey
2013-02-26Mod_subst: misc reformulationsletouzey
2013-02-24Reduced the noise level when dynlinking in bytecode mode or whenmdenes
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-19Classops : avoid some use of Gmapletouzey
2013-02-19Names: revised representation of constants and mutual_inductiveletouzey
2013-02-18use List.rev_map whenever possibleletouzey
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2013-02-01v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)herbelin
2013-01-28Fixed bug #2966 (de Bruijn error in computation of heads for coercions).herbelin
2013-01-28Actually adding backtrace handling.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-27Improving formatting of output of "Test table".herbelin
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of mod_bound_idppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
2012-12-08Finish patch for Hint Resolve, stopping to generate new constant names formsozeau
2012-11-25Monomorphization (library)ppedrot
2012-11-22Monomorphization (library)ppedrot
2012-11-13More monomorphizationsppedrot
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-29Fixed #2926:ppedrot
2012-10-29Removed many calls to OCaml generic equality. This was done byppedrot
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-06avoid using rectypes in nametab.mlletouzey
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-18Cleaning interface of Util.ppedrot
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
2012-09-15Some documentation and cleaning of CList and Util interfaces.ppedrot
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-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-08-24correct some ends of .mllib files (avoid a broken tolink.ml)letouzey
2012-08-24Assumption commands are now displayed as unsafe in Coqide.aspiwack