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
*
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
*
Parsing and printing of primitive projections, fix buggy behavior when
Matthieu Sozeau
2014-09-10
*
- Fix printing and parsing of primitive projections, including the Set
Matthieu Sozeau
2014-09-09
*
Removing dead code relative to the XML plugin.
Pierre-Marie Pédrot
2014-09-08
*
Print [Variant] types with the keyword [Variant].
Arnaud Spiwack
2014-09-04
*
Fixing bug #2818.
Pierre-Marie Pédrot
2014-09-03
*
Fix Declaremods.end_library (Closes: #3536)
Enrico Tassi
2014-09-02
*
Simplify even further the declaration of primitive projections,
Matthieu Sozeau
2014-08-30
*
Change the way primitive projections are declared to the kernel.
Matthieu Sozeau
2014-08-28
*
Fix computation of dangling constraints at the end of a proof (bug #3531).
Matthieu Sozeau
2014-08-25
*
instanciation is French, instantiation is English
Jason Gross
2014-08-25
[next]