index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
library
Commit message (
Expand
)
Author
Age
...
*
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
Enrico Tassi
2015-03-11
*
STM: proof state also includes meta counters
Enrico Tassi
2015-02-25
*
Refactoring in [Constr].
Arnaud Spiwack
2015-02-24
*
Fix some typos in comments.
Guillaume Melquiond
2015-02-23
*
Fixing 934761875 about optimizing Import of several libraries at once (thanks...
Hugo Herbelin
2015-02-23
*
Documenting the caveat of assumption printing in the mli.
Pierre-Marie Pédrot
2015-02-21
*
Tentative fix for bug #4078.
Pierre-Marie Pédrot
2015-02-21
*
More resilient implementation of Print Assumptions.
Pierre-Marie Pédrot
2015-02-21
*
Deprecated options issue a warning.
Pierre-Marie Pédrot
2015-02-17
*
Fixing bug #4053.
Pierre-Marie Pédrot
2015-02-17
*
Better comment for [type_of_global_unsafe].
Matthieu Sozeau
2015-02-16
*
Comment on the unsafe_ functions in Global.
Matthieu Sozeau
2015-02-16
*
Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior
Enrico Tassi
2015-02-14
*
Windows: open .vo files in binary mode
Enrico Tassi
2015-02-05
*
Properly set module names in presence of -Q. (Fix for bug #3958)
Guillaume Melquiond
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
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
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
*
Fix bug when discharging universe constraints coming from variables
Matthieu Sozeau
2015-01-13
*
fixup to vi -> vio renaming
Enrico Tassi
2015-01-12
*
Update headers.
Maxime Dénès
2015-01-12
*
Declarations.mli refactoring: module_type_body = module_body
Pierre Letouzey
2015-01-11
*
kernel/ind Change interface of declare_mind and declare_mutual
Matthieu Sozeau
2015-01-05
*
Forbid Require inside interactive modules and module types.
Maxime Dénès
2014-12-25
*
Summary: more surgery functions
Enrico Tassi
2014-12-17
*
Global: export the name of the summary entry
Enrico Tassi
2014-12-17
*
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
*
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-12-09
*
Reverting the following block of three commits:
Hugo Herbelin
2014-11-27
*
Registering strict implicit arguments systematically.
Hugo Herbelin
2014-11-26
*
Pass around information on the use of template polymorphism for
Matthieu Sozeau
2014-11-23
*
Universes.nf_evars_and_universes_opt_subst substitutes evars eagerly.
Pierre-Marie Pédrot
2014-11-10
*
Better error messages when unfreezing summary entries
Enrico Tassi
2014-10-30
*
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
*
selective join/export of the safe_environment
Enrico Tassi
2014-10-13
*
STM: simplify how the term part of a side effect is retrieved
Enrico Tassi
2014-10-13
*
library/opaqueTables: enable their use in interactive mode
Enrico Tassi
2014-10-13
*
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
Matthieu Sozeau
2014-10-11
*
Keyed unification option, compiling the whole standard library
Matthieu Sozeau
2014-09-27
*
Index keys instead of simply global references.
Matthieu Sozeau
2014-09-27
*
First version of keyed subterm selection in unification.
Matthieu Sozeau
2014-09-27
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Make eq_pattern_test/eq_test work up to the equivalence of primitive
Matthieu Sozeau
2014-09-24
*
Providing a -type-in-type option for collapsing the universe hierarchy.
Hugo Herbelin
2014-09-13
[prev]
[next]