coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Fix bug #4159	Matthieu Sozeau	2015-05-27
*	Disable precompilation for native_compute by default.	Guillaume Melquiond	2015-05-14
*	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
*	Tactical `progress` compares term up to potentially equalisable universes.	Arnaud Spiwack	2015-04-22
*	Extra fix to 934761875 and f4ee7ee31e4 on optimizing Import of several	Hugo Herbelin	2015-04-17
*	Strengthen minimization: it shouldn't set a universe u to a max if it	Matthieu Sozeau	2015-04-09
*	Make it possible for -R to override the existing implicit setting of a path.	Guillaume Melquiond	2015-04-02
*	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
*	Removing the unused root flag from loadpaths.	Pierre-Marie Pédrot	2015-03-31
*	A more reasonable implementation of Loadpath.	Pierre-Marie Pédrot	2015-03-31
*	Summary: fix code to detect functional values in summary	Enrico Tassi	2015-03-25
*	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
*	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