aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/library.ml
Commit message (Expand)AuthorAge
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
* [kernel] Patch allowing to disable VM reduction.Gravatar Emilio Jesus Gallego Arias2017-12-02
* [api] Miscellaneous consolidation + moves to engine.Gravatar Emilio Jesus Gallego Arias2017-11-21
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* [stm] [flags] Move document mode flags to the STM.Gravatar Emilio Jesus Gallego Arias2017-10-06
* Removing now useless former fix to #3333 (check valid module names).Gravatar Hugo Herbelin2017-09-12
* [flags] Remove XML output flag.Gravatar Emilio Jesus Gallego Arias2017-08-01
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [lib] Remove obsolete state-management function add_frozen_stateGravatar Emilio Jesus Gallego Arias2017-06-12
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 07:15:17 +0000