coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
...
*	First version of keyed subterm selection in unification.	Matthieu Sozeau	2014-09-27
\|
*	Fix test-suite file.	Matthieu Sozeau	2014-09-27
\|
*	Fix bug #3664 by refolding projections that don't reduce in cbn.	Matthieu Sozeau	2014-09-27
\|
*	Remove auto's use of dummy goal, use the proper sigma for pattern_of_constr.	Matthieu Sozeau	2014-09-27
\|
*	Fix semantics of matching with folded/unfolded projections to definitely	Matthieu Sozeau	2014-09-27
\| \| \| \|	avoid looping and be compatible with unfold.
*	Fix bug #3672, application of primitive projections as coercions.	Matthieu Sozeau	2014-09-27
\|
*	Fix bug 3662 by actually reducing primitive projections in cbv/compute.	Matthieu Sozeau	2014-09-27
\|
*	Bug fixed.	Matthieu Sozeau	2014-09-27
\|
*	Make pattern_of_constr typed so that we can infer the proper patterns	Matthieu Sozeau	2014-09-27
\| \| \| \| \| \|	for primitive projections, fixing bug #3661. Also fix expand_projection so that it does enough reduction to find the inductive type of its argument.
*	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau	2014-09-27
\| \| \| \| \| \| \| \|	so as to reproduce correctly the reduction behavior of existing projections, i.e. delta + iota. Make [projection] an abstract datatype in Names.ml, most of the patch is about using that abstraction. Fix unification.ml which tried canonical projections too early in presence of primitive projections.
*	Adapting to naming of evars.	Hugo Herbelin	2014-09-27
\|
*	Changed semantics of induction !id when a clause is given: don't	Hugo Herbelin	2014-09-27
\| \| \| \|	authoritatively erase non-generalized hypotheses dependent on id.
*	Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.	Pierre-Marie Pédrot	2014-09-27
\| \| \| \| \| \|	Most of the code from Goal.Refine and related was moved to the one file that was using it, wiz. tactics.ml. Some additional care should be taken to clean up even more the remaining code.
*	Adding a tclNEWGOALS primitive.	Pierre-Marie Pédrot	2014-09-26
\|
*	Hurkens.v: Fix a syntax error.	Arnaud Spiwack	2014-09-26
\| \| \|	Introduced in c74a70a73b3bf39394c551f1cdb224450bf77176.
*	Fix canonical structure resolution which was launched on the results of	Matthieu Sozeau	2014-09-26
\| \| \| \|	eta-expansion, creating a loop. This is now deactivated. Fixes bugs #3665 and #3667.
*	ClassicalFacts: adds a proof that weak excluded middle implies weak proof ↵	Arnaud Spiwack	2014-09-26
\| \| \| \| \|	irrelevance. Application of previous commit in Hurkens.v.
*	Hurkens.v: new paradox: type of modal propositions is not a retract.	Arnaud Spiwack	2014-09-26
\| \| \|	In particular there is no retract of the type of negative propositions in a negative proposition.
*	Hurkens.v: fix coqdoc formatting in a comment.	Arnaud Spiwack	2014-09-26
\|
*	Add a bunch of reproduction files for bugs.	Xavier Clerc	2014-09-26
\|
*	Add missing "Fail" to bug cases.	Xavier Clerc	2014-09-26
\|
*	Bug #3566 is fixed.	Xavier Clerc	2014-09-26
\|
*	Adding a test for bug #3653.	Pierre-Marie Pédrot	2014-09-26
\|
*	Test cases for closed bugs.	Xavier Clerc	2014-09-26
\|
*	Fix incorrect assert false in detyping.	Matthieu Sozeau	2014-09-25
\|
*	Revert changes of commit 4e1135fb315eab7 over file "plugins/micromega/sos.ml",	Xavier Clerc	2014-09-25
\| \| \| \|	as "\|\|" is actually redefined in "plugins/micromega/sos_lib.ml".
*	Add several reproduction files for bugs.	Xavier Clerc	2014-09-25
\|
*	Improve consistency of whitespace (beautifier).	Xavier Clerc	2014-09-25
\|
*	Remove some 'deprecated' warnings.	Xavier Clerc	2014-09-25
\|
*	Hurkens.v: update comments.	Arnaud Spiwack	2014-09-25
\|
*	Update test-suite files.	Matthieu Sozeau	2014-09-24
\|
*	Rename eq_constr functions in Evd to not break backward compatibility	Matthieu Sozeau	2014-09-24
\| \| \| \|	with existing ML code.
*	Return a Prop not an arbitrary Type, and correct a typo.	Matthieu Sozeau	2014-09-24
\|
*	Make eq_pattern_test/eq_test work up to the equivalence of primitive	Matthieu Sozeau	2014-09-24
\| \| \| \|	projections with their eta-expanded constant form.
*	Using an or_var rather than the hack with loc for coding a pure ident	Hugo Herbelin	2014-09-24
\| \| \| \|	as a disjunctive intropattern.
*	Added support for interpreting hyp lists in tactic notations.	Hugo Herbelin	2014-09-24
\|
*	Hurkens.v: show proofs in coqdoc.	Arnaud Spiwack	2014-09-24
\|
*	Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].	Arnaud Spiwack	2014-09-24
\|
*	Hurkens.v: coqdoc documentation.	Arnaud Spiwack	2014-09-24
\|
*	A new version of Hurkens.v.	Arnaud Spiwack	2014-09-24
\| \| \| \|	Adds a more generic and modular proof of Hurkens, where a shallow embedding of U- is given in the most general way. Subsumes all the previous proofs, opens the way to new proofs.
*	Make the retroknowledge marshalable.	Arnaud Spiwack	2014-09-24
\| \| \| \| \| \|	Essential for parallel processing of Coq documents. It is a fairly straightforward change but a tad tedious, I may have introduced some bugs in the process.
*	Fix a message.	Arnaud Spiwack	2014-09-24
\|
*	coqtop -emacs: do not declare "still unfocused goals" as an "infomsg".	Arnaud Spiwack	2014-09-24
\| \| \|	This prevented the message from being silent when jumping ahead in a file. Fixes #3636.
*	Fix bug #3656.	Matthieu Sozeau	2014-09-23
\| \| \| \| \| \|	Maintain the user-level view of primitive projections, disallow manual unfolding and do not let hnf give the eta-expanded form.
*	ATBR can't compile without the fix, as it uses setoid_rewrite to rewrite	Matthieu Sozeau	2014-09-23
\| \| \| \|	under binders. This might incur a significant time penalty.
*	Fix bug in setoid_rewrite introduced by PMP's commits, which was creating	Matthieu Sozeau	2014-09-23
\| \| \| \| \| \|	two versions of the rewriting lemma, keeping useless evars around. This can now happen only when the rewrite lemma is used under binders... Fix to do next.
*	adds general facts in the Reals library, whose need was detected in	Yves Bertot	2014-09-23
\| \| \| \|	experiments about computing PI
*	Correction of error message (bug 3359)	Julien Forest	2014-09-22
\|
*	Fixing bug 3951	Julien Forest	2014-09-22
\|
*	Rewrite.apply_lemma is written in state passing style.	Pierre-Marie Pédrot	2014-09-21
\| \| \| \|	This removes a use of Evd.merge.