aboutsummaryrefslogtreecommitdiffhomepage
path: root/library
Commit message (Expand)AuthorAge
* Minor simplifications in Declaremods and Safe_typingGravatar letouzey2013-04-15
* Declaremods: drop some useless stuff (slight gain in vo size)Gravatar letouzey2013-04-15
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* Safe_typing+Libary: use some arrays instead of lists in vo structuresGravatar letouzey2013-03-28
* Synchronizing loadpath with the backtrack mechanism.Gravatar ppedrot2013-03-26
* Moved the Loadpath part of Library to its own file, and documentedGravatar ppedrot2013-03-26
* Minor code cleaning in CArray / CList.Gravatar ppedrot2013-03-23
* Removing mandatory suffixes for library files.Gravatar ppedrot2013-03-21
* Modules and ppvernac, sequel of Enrico's commit 16261Gravatar letouzey2013-03-13
* Declaremods: a few syntactic improvementsGravatar letouzey2013-03-13
* 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