index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
/
library.ml
Commit message (
Expand
)
Author
Age
...
*
Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of several
Hugo Herbelin
2015-04-17
*
From X Require Y looks for X with absolute path, disregarding -R.
Pierre-Marie Pédrot
2015-04-01
*
Removing a probably incorrect on-the-fly require in a tactic.
Pierre-Marie Pédrot
2015-04-01
*
Dedicated type for on-demand objects in Library.
Pierre-Marie Pédrot
2015-03-23
*
Removing the whole library content from the summary.
Pierre-Marie Pédrot
2015-03-16
*
More invariants in Library.
Pierre-Marie Pédrot
2015-03-16
*
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
Enrico Tassi
2015-03-11
*
Fixing 934761875 about optimizing Import of several libraries at once (thanks...
Hugo Herbelin
2015-02-23
*
Windows: open .vo files in binary mode
Enrico Tassi
2015-02-05
*
Optimized Import/Export the same way as Require Import/Export was
Hugo Herbelin
2015-02-04
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
Remove dead code.
Maxime Dénès
2015-01-17
*
Partially revert "Forbid Require inside interactive modules and module types."
Maxime Dénès
2015-01-17
*
Avoid compilation warning... might not be the best fix though.
Matthieu Sozeau
2015-01-17
*
Made -print-mod-uid more silent and robust.
Maxime Dénès
2015-01-13
*
fixup to vi -> vio renaming
Enrico Tassi
2015-01-12
*
Update headers.
Maxime Dénès
2015-01-12
*
Forbid Require inside interactive modules and module types.
Maxime Dénès
2014-12-25
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Fix for #3154: use CUnix.sys_command to call native compiler.
Maxime Dénès
2014-12-16
*
When loading libraries, feed back dependencies.
Carst Tankink
2014-10-13
*
STM: primitives to snapshot a .vi while in interactive mode
Enrico Tassi
2014-10-13
*
library/opaqueTables: enable their use in interactive mode
Enrico Tassi
2014-10-13
*
Removing dead code relative to the XML plugin.
Pierre-Marie Pédrot
2014-09-08
*
Feedback: LoadedFile + Goals
Enrico Tassi
2014-07-11
*
Checking that a library name is valid before compilation.
Pierre-Marie Pédrot
2014-06-16
*
Deprecate options -dont, -lazy, -force-load-proofs.
Guillaume Melquiond
2014-06-13
*
Fix native_compute for systems with a limited size for the command line.
Guillaume Melquiond
2014-05-22
*
Eliminating a potentially quadratic behaviour in Require, by using maps
Pierre-Marie Pédrot
2014-05-11
*
- Fix bug preventing apply from unfolding Fixpoints.
Matthieu Sozeau
2014-05-06
*
Adapt universe polymorphic branch to new handling of futures for delayed proofs.
Matthieu Sozeau
2014-05-06
*
Native compiler: hide compiled files in a .coq-native subdirectory.
Maxime Dénès
2014-04-29
*
STM: make -async-proofs on work from coqc too
Enrico Tassi
2014-03-18
*
vi2vo: universes handling finally fixed
Enrico Tassi
2014-03-11
*
Fix lookup of native files when option -R is missing.
Guillaume Melquiond
2014-03-07
*
Library: when compiling multiple files, reset the opaque tables
Enrico Tassi
2014-02-26
*
Lazyconstr -> Opaqueproof
Enrico Tassi
2014-02-26
*
New compilation mode -vi2vo
Enrico Tassi
2014-02-26
*
coqtop: -check-vi-tasks and -schedule-vi-checking
Enrico Tassi
2014-01-05
*
.vi files: .vo files without proofs
Enrico Tassi
2014-01-04
*
Print logical name rather than path (thus allowing reproducible tests).
xclerc
2013-12-02
*
Native compiler: library compilation errors are now non fatal.
mdenes
2013-10-28
*
More monomorphic List.mem + List.assoc + ...
letouzey
2013-10-24
*
Turn many List.assoc into List.assoc_f
letouzey
2013-10-24
*
Removing a bunch of generic equalities.
ppedrot
2013-09-27
*
Get rid of the uses of deprecated OCaml elements (still remaining compatible ...
xclerc
2013-09-19
*
Change in vo format : digest aren't Marshalled anymore
letouzey
2013-08-22
*
enhance marshallable option for freeze (minor TODO in safe_typing)
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Use the Hook module here and there.
ppedrot
2013-05-12
[prev]
[next]