coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-07
\|\
\| *	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-07
\| \|\
\| * \|	micromega : more robust generation of proof terms	Frédéric Besson	2016-09-07
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Assert a purely arihtmetic sub-goal that is proved independently by reflexion. (This reduces the stress on the conversion test) - Does not use 'abstract' anymore (more natural proof-term) - Fix a parsing bug (certain terms in Prop where not recognized)
\| \| *	Test file for #5065 - Anomaly: Not a proof by induction	Maxime Dénès	2016-09-05
\| \| \|
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-09-02
\|\\| \|
\| * \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-09-02
\| \|\\|
\| \| *	Fix test-suite after Frédéric's 6231f07b2.	Maxime Dénès	2016-09-01
\| \| \|
\| * \|	Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'.	Frédéric Besson	2016-08-31
\| \| \| \| \| \| \| \| \| \| \| \|	If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative.
\| \| *	Fix bug #5043: [Admitted] lemmas pick up section variables.	Pierre-Marie Pédrot	2016-08-31
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We add a flag Keep Admitted Variables that allows to recover the legacy v8.4 behaviour of admitted lemmas. The statement of such lemmas did not depend on the current context variables.
\| * \|	Fixing output test-suite after warning for inner Requires.	Pierre-Marie Pédrot	2016-08-30
\| \| \|
\| * \|	Fix bug #4893: not_evar: unexpected failure in 8.5pl1.	Pierre-Marie Pédrot	2016-08-30
\| \| \|
\| * \|	plugin micromega : nra also handles non-linear rational arithmetic over Q ↵	Frédéric Besson	2016-08-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R.
\| * \|	Fix bug #3920: eapply masks an hypothesis name.	Pierre-Marie Pédrot	2016-08-30
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The problem came from the fact that the legacy beta-reduction occurring after a rewrite was wrongly applied to the side-conditions of the rewriting step. We restrict it to the correct goal in this patch.
\| * \|	Fix bug #4764: Syntactic notation externalization breaks.	Pierre-Marie Pédrot	2016-08-28
\| \| \|
* \| \|	Merge remote-tracking branch 'v8.6' into trunk	Matej Kosik	2016-08-25
\|\\| \|
\| * \|	Fix bug #4904: [Import] does not load intermediately unqualified names of ↵	Pierre-Marie Pédrot	2016-08-23
\| \| \| \| \| \| \| \| \| \| \| \|	aliases.
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-08-21
\|\\| \|
\| * \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-21
\| \|\\|
\| \| *	Fixing an anomaly in printing a unification error message.	Hugo Herbelin	2016-08-20
\| \| \|
\| * \|	Test file for bug #4187.	Pierre-Marie Pédrot	2016-08-19
\| \| \|
\| * \|	Merge remote-tracking branch 'origin/pr/246' into v8.6	Matthieu Sozeau	2016-08-19
\| \|\ \
\| * \| \|	Adding a test for bug #4653.	Pierre-Marie Pédrot	2016-08-18
\| \| \| \|
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-08-17
\|\\| \| \|
\| * \| \|	Fixing #3070 ("subst" taking properly into account chains of dependencies).	Hugo Herbelin	2016-08-17
\| \| \| \|
\| * \| \|	Merge branch 'v8.5' into v8.6	Pierre-Marie Pédrot	2016-08-16
\| \|\ \ \ \| \| \| \|/ \| \| \|/\|
\| \| * \|	Fix bug #4673: regression in setoid_rewrite.	Matthieu Sozeau	2016-07-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Modulo delta for types should be fully transparent.
\| * \| \|	Merge remote-tracking branch 'gforge/v8.5' into v8.6	Matthieu Sozeau	2016-07-29
\| \|\\| \|
\| \| * \|	Fix bug #3886, generation of obligations of fixes	Matthieu Sozeau	2016-07-29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This partially reverts c14ccd1b8a3855d4eb369be311d4b36a355e46c1
\| \| * \|	Fix #4769, univ poly and elim schemes in sections	Matthieu Sozeau	2016-07-29
\| \| \| \|
* \| \| \|	Merge branch 'v8.6' into trunk	Pierre Letouzey	2016-07-26
\|\\| \| \|
\| \| * \|	Fix bug #4754, allow conversion problems to remain	Matthieu Sozeau	2016-07-26
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	when checking that the rewrite relation is homogeneous in setoid_rewrite.
\| * \| \|	Fix bug #4679, weakened setoid_rewrite unification	Matthieu Sozeau	2016-07-21
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It should use evar instantiations eagerly during unification of the lhs of the lemma, as in 8.4.
* \| \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-07-20
\|\\| \| \|
\| \| * \|	Fix bug #4780: universe leak in letin_tac	Matthieu Sozeau	2016-07-20
\| \| \| \|
\| * \| \|	Fix bug #4780: universe leak in letin_tac	Matthieu Sozeau	2016-07-20
\| \| \| \|
\| \| * \|	Fix Errors.out missing a dot...	Matthieu Sozeau	2016-07-19
\| \| \| \|
\| * \| \|	Some extra fixes in printing patterns in binders.	Hugo Herbelin	2016-07-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- typo in notation_ops.ml - factorization of patterns in ppconstr.ml - update of test-suite - printing of cast of a binding pattern if in mode "printing all" The question of whether or not to print the type of a binding pattern by default seems open to me.
\| * \| \|	Taking into account binding patterns when agglutinating sequences of binders.	Hugo Herbelin	2016-07-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Supporting accordingly printing of sequences of binders including binding patterns.
\| * \| \|	Fixing missing parentheses in printing of patterns in binders.	Hugo Herbelin	2016-07-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	(In agreement with Daniel.)
\| * \| \|	Notations: fixing multiple binders used as terms in reverse order.	Hugo Herbelin	2016-07-19
\| \| \| \|
\| * \| \|	Removing a source of clash with multiple recursive patterns in notations.	Hugo Herbelin	2016-07-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The same variable name was used to collect the binders and the successive steps of matching one binder, resulting in unexpected attempts for merging in the presence of multiple occurrence of the same recursive pattern. An amusing side-effect: when eta-expanding for a notation with recursive binders, it is the second variable of the "x .. y" which is used to invent a name rather than the first one.
\| * \| \|	A new step on using alpha-conversion in printing notations.	Hugo Herbelin	2016-07-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	A couple of bugs have been found. Example #4932 is now printing correctly in the presence of multiple binders (when no let-in, no irrefutable patterns).
\| * \| \|	Marking bug #3383 as solved.	Pierre-Marie Pédrot	2016-07-18
\| \| \| \|
\| * \| \|	Fix bug #4923: Warning: appcontext is deprecated.	Pierre-Marie Pédrot	2016-07-18
\| \| \| \|
\| * \| \|	Partial fix to #4592 (notation requiring alpha-conversion for printing).	Hugo Herbelin	2016-07-17
\| \| \| \|
\| * \| \|	More examples of recursive notations, with emphasis in reference manual.	Hugo Herbelin	2016-07-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Further work would include: - Identify binders up to alpha-conversion (see #4932 with a list of binders of length at least 2, or #4592 on printing notations such as ex2). A cool example that one could also consider supporting: - Notation "[[ a , .. , b \| .. \| a , .. , b ]]" := (cons (cons a .. (cons b nil) ..) .. (cons a .. (cons b nil) ..) ..).
\| * \| \|	Fixing a bug in recognizing a recursive pattern of notations	Hugo Herbelin	2016-07-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	immediately in the scope of another recursive pattern.
\| * \| \|	Fixing interpretation of notations w/ opposite instances of a recursive pattern.	Hugo Herbelin	2016-07-17
\| \| \| \|
\| * \| \|	Fixing printing of notations with several instances of a recursive pattern.	Hugo Herbelin	2016-07-17
\| \| \| \|
\| * \| \|	Fixing #4932 (anomaly when using binders as terms in recursive notations).	Hugo Herbelin	2016-07-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This application was actually not anticipated. It is nice and was not too difficult to support. Design for pattern binders maybe to clarify. When seing pat(x1,..,xn) as a term, I just reused pat(x1,..,xn), but maybe it is worth using the variable aliasing the pattern, for more a concise notation. But at the same time, this means exposing the internal name of the alias which is not so elegant.