coq - The formal proof system

Age	Commit message (Expand)	Author
2014-10-30	Better error messages when unfreezing summary entries	Enrico Tassi
2014-10-30	Fix backtracking issue in Defined (Close 3780)	Enrico Tassi
2014-10-28	Haskell extraction: use explicit -XMagicHash instead of -fglasgow-exts	Nickolai Zeldovich
2014-10-28	Haskell extraction: put unsafeCoerce type declaration later	Nickolai Zeldovich
2014-10-28	Allow camlp5 to have version numbers like "6.09-exp"	jbapple
2014-10-27	Cleaning and documenting Clenv.make_evar_clause	Pierre-Marie Pédrot
2014-10-27	Removing dead code from Evd.	Pierre-Marie Pédrot
2014-10-27	Removing the Evd.diff function.	Pierre-Marie Pédrot
2014-10-27	Removing the last Evd.diff from Hints.	Pierre-Marie Pédrot
2014-10-27	Removing the Evd.merge function.	Pierre-Marie Pédrot
2014-10-27	Removing an Evd.merge in Newring.	Pierre-Marie Pédrot
2014-10-27	Fixes for PG (Close 3763, 3770)	Enrico Tassi
2014-10-27	Make sure that Logic/ExtensionalityFacts gets compiled.	Guillaume Melquiond
2014-10-27	Fix some typos.	Guillaume Melquiond
2014-10-27	Use the url package, since coqdoc generates \url commands.	Guillaume Melquiond
2014-10-27	Making destruct on idents with maximal implicit arguments working, by	Hugo Herbelin
2014-10-27	Ensuring compatibility when an hypothesis used for destruct is	Hugo Herbelin
2014-10-27	Fixing evars lost in interpretation of eliminator of destruct.	Hugo Herbelin
2014-10-27	Fixing clash in test destruct.v.	Hugo Herbelin
2014-10-27	Dead code	Hugo Herbelin
2014-10-27	Fix some typos in comments.	Guillaume Melquiond
2014-10-26	Preventing potential evar leak in Rewrite.	Pierre-Marie Pédrot
2014-10-26	Applying like-first selection for destruct in hypotheses.	Hugo Herbelin
2014-10-26	Fixing destruct/induction with a using clause on a non-inductive type,	Hugo Herbelin
2014-10-26	Dead code + typo.	Hugo Herbelin
2014-10-25	Changed implementation of lib/heap.ml to use Braun trees	Jean-Christophe Filliatre
2014-10-25	This commit introduces changes in induction and destruct.	Hugo Herbelin
2014-10-25	VarInstance are also goals.	Hugo Herbelin
2014-10-24	Install index_urls.txt in a location where coqide might actually find it.	Guillaume Melquiond
2014-10-24	Fix generation of the index_urls.txt file.	Guillaume Melquiond
2014-10-24	Change reduction_of_red_expr to return an e_reduction_function returning	Matthieu Sozeau
2014-10-24	Remove an ununsed pattern and commented code in the kernel.	Matthieu Sozeau
2014-10-24	Apparently, the former refine was simplifying in hypotheses too.	Hugo Herbelin
2014-10-24	Documenting some incompatibilities in (non) Import of ML tactics,	Hugo Herbelin
2014-10-24	Fixing order of hypothesis in goal hypotheses compaction for coqtop.	Hugo Herbelin
2014-10-24	Addressing report #3279 (inconsistency of behavior of the -> and <-	Hugo Herbelin
2014-10-24	Fix retroknowledge for int31 division.	Maxime Dénès
2014-10-24	-help failing (fix 3762)	Enrico Tassi
2014-10-24	Fix typo in documentation of the [repeat] tactical.	Arnaud Spiwack
2014-10-24	No hash consing across calls to the native compiler.	Maxime Dénès
2014-10-23	Fixing order of declarations in the function which compacts variables	Hugo Herbelin
2014-10-23	Fixing clash in output test-suite Cases.	Hugo Herbelin
2014-10-23	Taking into account factorization of consecutive names of same types	Hugo Herbelin
2014-10-23	fix parsing of ---- +++++ ***** in CoqIDE	Enrico Tassi
2014-10-23	Monad: change the error managing of two-list combinators.	Arnaud Spiwack
2014-10-23	Evd.future_goals: forgot to revert the list in two places.	Arnaud Spiwack
2014-10-23	Proofview: forgot to change an exception after refactoring in ( 9f51aafebd5f3...	Arnaud Spiwack
2014-10-22	Bugfix 3604 : more robust Unix.lockf	Frédéric Besson
2014-10-22	Fixing typo in output test Notations.	Hugo Herbelin
2014-10-22	Pushing Pierre's factorization of names in goal context printing from	Hugo Herbelin