coq - The formal proof system

Age	Commit message (Expand)	Author
2015-02-05	Properly set module names in presence of -Q. (Fix for bug #3958)	Guillaume Melquiond
2015-02-04	Optimized Import/Export the same way as Require Import/Export was	Hugo Herbelin
2015-02-04	Tactic Notation: use stable unique key for notations (Close: 3970)	Enrico Tassi
2015-02-03	Revert "Tactic Notation: use stable unique key for notations (Close: 3970)"	Enrico Tassi
2015-02-03	Tactic Notation: use stable unique key for notations (Close: 3970)	Enrico Tassi
2015-02-03	spit module path using / as directory separator	Enrico Tassi
2015-02-02	Removing dead code.	Pierre-Marie Pédrot
2015-01-29	Prevent spurious warnings about Arguments.	Guillaume Melquiond
2015-01-24	Equality Schemes options: reverting commit ff9f94634 which is	Hugo Herbelin
2015-01-24	Isolate a function for printing evar sets.	Hugo Herbelin
2015-01-21	Add the possibility of defining opaque terms with program.	mlasson
2015-01-17	Univs: proper printing of global and local universe names (only	Matthieu Sozeau
2015-01-17	Make native compiler handle universe polymorphic definitions.	Maxime Dénès
2015-01-15	Make -print-mod-uid accept a list of files.	Maxime Dénès
2015-01-13	Made -print-mod-uid more silent and robust.	Maxime Dénès
2015-01-12	Add -no-native-compiler flag to list dumped by --help.	Maxime Dénès
2015-01-12	Update headers.	Maxime Dénès
2015-01-11	Avoiding a redundant information in unification error message.	Hugo Herbelin
2015-01-08	Avoiding introducing yet another convention in naming files.	Hugo Herbelin
2015-01-06	rename: vi -> vio	Enrico Tassi
2015-01-06	Fix some documentation typos.	Guillaume Melquiond
2015-01-05	kernel/ind Change interface of declare_mind and declare_mutual	Matthieu Sozeau
2015-01-05	In Show Universes, print universes before normalization.	Matthieu Sozeau
2014-12-29	Fixing bug #3632 for good.	Pierre-Marie Pédrot
2014-12-29	Proof using: do not clear letins (unless they use a cleared var)	Enrico Tassi
2014-12-28	Proof using: call "clear" to remove from sight the vars not selected	Enrico Tassi
2014-12-28	remove debug prints (leftover)	Enrico Tassi
2014-12-19	Better doc and a few fixes for Proof using.	Enrico Tassi
2014-12-18	Proof using: New vernacular to name sets of section variables	Enrico Tassi
2014-12-17	STM: rename and simplify flags	Enrico Tassi
2014-12-17	Arguments: warn only if no option is given (Close 3860)	Enrico Tassi
2014-12-16	Fixing CAMLP4 compilation.	Pierre-Marie Pédrot
2014-12-16	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot
2014-12-16	Error messages of Searchxxx are coherent with goal selector.	Pierre Courtieu
2014-12-15	Failing on unbound notation variable in notation level modifiers	Hugo Herbelin
2014-12-15	About now accepts hypothesis names and goal selector.	Pierre Courtieu
2014-12-14	Util.un_op -> Option.default	Pierre Boutillier
2014-12-12	Searchxxx now interpret patterns in goal environment if any.	Pierre Courtieu
2014-12-12	Searchxxx now search also the hypothesis and support goal selector.	Pierre Courtieu
2014-12-11	Added a CannotSolveConstraint unification error and made experiments	Hugo Herbelin
2014-12-11	Tentatively more informative report of failure when inferring	Hugo Herbelin
2014-12-09	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey
2014-12-07	Improved tracking of the origin of evars.	Hugo Herbelin
2014-12-04	Improving error message when one instance-hole is not found.	Hugo Herbelin
2014-12-04	Reactivating option "Set Printing Existential Instances" for asking printing ...	Hugo Herbelin
2014-12-03	Slight improving of a unification error message.	Hugo Herbelin
2014-11-30	Adding a Refine Instance Mode option that allows to deactivate the	Pierre-Marie Pédrot
2014-11-27	async_queries_* merged with async_proofs_*	Enrico Tassi
2014-11-27	Feedback: API cleaned up, documented and made user extensible	Enrico Tassi
2014-11-24	Plugging console highlighting in for toplevel and compilation error messages.	Pierre-Marie Pédrot