aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
Commit message (Expand)AuthorAge
* Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\
* | Emit a warning on Require inside a module.Gravatar Maxime Dénès2016-08-30
* | Send Dependency feedback only if file not already loaded.Gravatar Maxime Dénès2016-08-29
* | Fix bug #4750: Change format of inconsistent assumptions message.Gravatar Pierre-Marie Pédrot2016-08-28
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* Merge remote-tracking branch 'origin/pr/166' into trunkGravatar Enrico Tassi2016-06-14
|\
* \ Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\ \
| * | Fix incorrect checking of library checksums.Gravatar Maxime Dénès2016-06-05
* | | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
| | * coqc: support -o option to specify output file nameGravatar Enrico Tassi2016-05-19
| |/ |/|
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-05
|\|
| * Fix #4607: do not read native code files if native compiler was disabled.Gravatar Maxime Dénès2016-03-04
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| * Hooks for a third-party XML plugin. Contributed by Claudio Sacerdoti Coen.Gravatar Maxime Dénès2016-01-15
* | Remove Library.mem, which is pointless since 8.5.Gravatar Guillaume Melquiond2015-12-31
* | Avoid a pointless conversion/copy.Gravatar Guillaume Melquiond2015-12-22
* | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
* | Move the From logic to Loadpath.expand_path.Gravatar Guillaume Melquiond2015-12-22
* | Do not query module files that have already been loaded.Gravatar Guillaume Melquiond2015-12-22
|/
* Fix dumb typo.Gravatar Guillaume Melquiond2015-09-29
* Make the interface of System.raw_extern_intern much saner.Gravatar Guillaume Melquiond2015-09-29
* Prevent States.intern_state and System.extern_intern from looking up files in...Gravatar Guillaume Melquiond2015-09-29
* Remove some uses of Loadpath.get_paths.Gravatar Guillaume Melquiond2015-09-29
* Make -load-vernac-object respect the loadpath.Gravatar Guillaume Melquiond2015-09-28
* The -require option now accepts a logical path instead of a physical one.Gravatar Pierre-Marie Pédrot2015-09-25
* The -compile option now accepts ".v" files and outputs a warning otherwise.Gravatar Pierre-Marie Pédrot2015-09-25
* Add an if_verbose for "Fetching opaque proofs ..."Gravatar mlasson2015-09-03
* Improve semantics of -native-compiler flag.Gravatar Maxime Dénès2015-07-09
* On-demand Require.Gravatar Pierre-Marie Pédrot2015-06-24
* Splitting the library representation on disk in two.Gravatar Pierre-Marie Pédrot2015-06-24
* Disable precompilation for native_compute by default.Gravatar Guillaume Melquiond2015-05-14
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of severalGravatar Hugo Herbelin2015-04-17
* From X Require Y looks for X with absolute path, disregarding -R.Gravatar Pierre-Marie Pédrot2015-04-01
* Removing a probably incorrect on-the-fly require in a tactic.Gravatar Pierre-Marie Pédrot2015-04-01
* Dedicated type for on-demand objects in Library.Gravatar Pierre-Marie Pédrot2015-03-23
* Removing the whole library content from the summary.Gravatar Pierre-Marie Pédrot2015-03-16
* More invariants in Library.Gravatar Pierre-Marie Pédrot2015-03-16
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Fixing 934761875 about optimizing Import of several libraries at once (thanks...Gravatar Hugo Herbelin2015-02-23
* Windows: open .vo files in binary modeGravatar Enrico Tassi2015-02-05
* Optimized Import/Export the same way as Require Import/Export wasGravatar Hugo Herbelin2015-02-04
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Remove dead code.Gravatar Maxime Dénès2015-01-17
* Partially revert "Forbid Require inside interactive modules and module types."Gravatar Maxime Dénès2015-01-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-03 08:54:11 +0000