aboutsummaryrefslogtreecommitdiff
path: root/library/library.ml
AgeCommit message (Expand)Author
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
2014-12-25Forbid Require inside interactive modules and module types.Maxime Dénès
2014-12-16Getting rid of Exninfo hacks.Pierre-Marie Pédrot
2014-12-16Fix for #3154: use CUnix.sys_command to call native compiler.Maxime Dénès
2014-10-13When loading libraries, feed back dependencies.Carst Tankink
2014-10-13STM: primitives to snapshot a .vi while in interactive modeEnrico Tassi
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-09-08Removing dead code relative to the XML plugin.Pierre-Marie Pédrot
2014-07-11Feedback: LoadedFile + GoalsEnrico Tassi
2014-06-16Checking that a library name is valid before compilation.Pierre-Marie Pédrot
2014-06-13Deprecate options -dont, -lazy, -force-load-proofs.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 01:51:35 +0000