aboutsummaryrefslogtreecommitdiff
path: root/library/library.ml
AgeCommit message (Expand)Author
2016-08-30Emit a warning on Require inside a module.Maxime Dénès
2016-08-29Send Dependency feedback only if file not already loaded.Maxime Dénès
2016-08-28Fix bug #4750: Change format of inconsistent assumptions message.Pierre-Marie Pédrot
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-29A new infrastructure for warnings.Maxime Dénès
2016-06-14Merge remote-tracking branch 'origin/pr/166' into trunkEnrico Tassi
2016-06-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-05Fix incorrect checking of library checksums.Maxime Dénès
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-19coqc: support -o option to specify output file nameEnrico Tassi
2016-03-05Merge branch 'v8.5'Pierre-Marie Pédrot
2016-03-04Fix #4607: do not read native code files if native compiler was disabled.Maxime Dénès
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-15Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Maxime Dénès
2015-12-31Remove Library.mem, which is pointless since 8.5.Guillaume Melquiond
2015-12-22Avoid a pointless conversion/copy.Guillaume Melquiond
2015-12-22Do not compose "str" and "to_string" whenever possible.Guillaume Melquiond
2015-12-22Move the From logic to Loadpath.expand_path.Guillaume Melquiond
2015-12-22Do not query module files that have already been loaded.Guillaume Melquiond
2015-09-29Fix dumb typo.Guillaume Melquiond
2015-09-29Make the interface of System.raw_extern_intern much saner.Guillaume Melquiond
2015-09-29Prevent States.intern_state and System.extern_intern from looking up files in...Guillaume Melquiond
2015-09-29Remove some uses of Loadpath.get_paths.Guillaume Melquiond
2015-09-28Make -load-vernac-object respect the loadpath.Guillaume Melquiond
2015-09-25The -require option now accepts a logical path instead of a physical one.Pierre-Marie Pédrot
2015-09-25The -compile option now accepts ".v" files and outputs a warning otherwise.Pierre-Marie Pédrot
2015-09-03Add an if_verbose for "Fetching opaque proofs ..."mlasson
2015-07-09Improve semantics of -native-compiler flag.Maxime Dénès
2015-06-24On-demand Require.Pierre-Marie Pédrot
2015-06-24Splitting the library representation on disk in two.Pierre-Marie Pédrot
2015-05-14Disable precompilation for native_compute by default.Guillaume Melquiond
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-04-17Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of severalHugo Herbelin
2015-04-01From X Require Y looks for X with absolute path, disregarding -R.Pierre-Marie Pédrot
2015-04-01Removing a probably incorrect on-the-fly require in a tactic.Pierre-Marie Pédrot
2015-03-23Dedicated type for on-demand objects in Library.Pierre-Marie Pédrot
2015-03-16Removing the whole library content from the summary.Pierre-Marie Pédrot
2015-03-16More invariants in Library.Pierre-Marie Pédrot
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-02-23Fixing 934761875 about optimizing Import of several libraries at once (thanks...Hugo Herbelin
2015-02-05Windows: open .vo files in binary modeEnrico Tassi
2015-02-04Optimized Import/Export the same way as Require Import/Export wasHugo Herbelin
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-17Remove dead code.Maxime Dénès
2015-01-17Partially revert "Forbid Require inside interactive modules and module types."Maxime Dénès
2015-01-17Avoid compilation warning... might not be the best fix though.Matthieu Sozeau
2015-01-13Made -print-mod-uid more silent and robust.Maxime Dénès
2015-01-12fixup to vi -> vio renamingEnrico Tassi
2015-01-12Update headers.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 17:26:18 +0000