aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Restrict (try...with...) to avoid catching critical exn (part 8)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 6)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 5)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 1)Gravatar letouzey2013-03-12
* Added a Local Definition vernacular command. This type of definitionGravatar ppedrot2013-03-11
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Names: shortcuts for building {kn, constant, mind} with empty sectionsGravatar letouzey2013-02-26
* Mod_subst: misc reformulationsGravatar letouzey2013-02-26
* Reduced the noise level when dynlinking in bytecode mode or whenGravatar mdenes2013-02-24
* avoid (Int.equal (cmp ...) 0) when a boolean equality existsGravatar letouzey2013-02-19
* Dir_path --> DirPathGravatar letouzey2013-02-19
* module_path --> ModPath.t, kernel_name --> KerName.tGravatar letouzey2013-02-19
* Classops : avoid some use of GmapGravatar letouzey2013-02-19
* Names: revised representation of constants and mutual_inductiveGravatar letouzey2013-02-19
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
* v8.4: Granting bug/wish #2976 (turning anomaly on input_value into nice message)Gravatar herbelin2013-02-01
* Fixed bug #2966 (de Bruijn error in computation of heads for coercions).Gravatar herbelin2013-01-28
* Actually adding backtrace handling.Gravatar ppedrot2013-01-28
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Improving formatting of output of "Test table".Gravatar herbelin2013-01-27
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of mod_bound_idGravatar ppedrot2012-12-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Stringset and Stringmap to String namespace.Gravatar ppedrot2012-12-14
* Finish patch for Hint Resolve, stopping to generate new constant names forGravatar msozeau2012-12-08
* Monomorphization (library)Gravatar ppedrot2012-11-25
* Monomorphization (library)Gravatar ppedrot2012-11-22
* More monomorphizationsGravatar ppedrot2012-11-13
* Monomorphized a lot of equalities over OCaml integers, thanks toGravatar ppedrot2012-11-08
* Fixed #2926:Gravatar ppedrot2012-10-29
* Removed many calls to OCaml generic equality. This was done byGravatar ppedrot2012-10-29
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* avoid using rectypes in nametab.mlGravatar letouzey2012-10-06
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
* 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
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* correct some ends of .mllib files (avoid a broken tolink.ml)Gravatar letouzey2012-08-24
* Assumption commands are now displayed as unsafe in Coqide.Gravatar aspiwack2012-08-24
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22