aboutsummaryrefslogtreecommitdiff
path: root/library
AgeCommit message (Expand)Author
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
2013-03-28Safe_typing+Libary: use some arrays instead of lists in vo structuresletouzey
2013-03-26Synchronizing loadpath with the backtrack mechanism.ppedrot
2013-03-26Moved the Loadpath part of Library to its own file, and documentedppedrot
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-03-21Removing mandatory suffixes for library files.ppedrot
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