coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	TCs: Properly handle Hint Extern with conclusions of the form _ -> _	Matthieu Sozeau	2015-01-13
\| \| \| \| \|	in typeclasses eauto, remaining compatible with eauto and still producing eta-reduced applications for Hint Resolves. Fixes bug #3794.
*	Fix test-suite file, we were testing that no anomaly was raised	Matthieu Sozeau	2015-01-13
\| \| \| \|	and this is the case now.
*	Fix files in test-suite having to do with Require inside modules.	Maxime Dénès	2015-01-12
\|
*	Update headers.	Maxime Dénès	2015-01-12
\|
*	Update test for #3363 now that Require is forbidden inside modules.	Maxime Dénès	2015-01-12
\|
*	Fixing name of evars in output test Notation.v.	Hugo Herbelin	2015-01-12
\|
*	Extraction: discard code unnecessary to fulfill a module signature	Pierre Letouzey	2015-01-11
\|
*	STM: fix handling of side effects in vio2vo	Enrico Tassi	2015-01-09
\|
*	rename: vi -> vio	Enrico Tassi	2015-01-06
\|
*	Fixing test for bug #2830.	Pierre-Marie Pédrot	2015-01-06
\|
*	kernel/ind Change interface of declare_mind and declare_mutual	Matthieu Sozeau	2015-01-05
\| \| \| \| \| \|	Removing unused argument and fixing bug #3899, now warning when a record cannot be made primitive in Set Primitive Projections mode because it has no projection or at least one undefinable projection.
*	Adapting two files from test-suite to now forbidden Require's in modules.	Hugo Herbelin	2015-01-04
\| \| \| \| \|	Status of 335 and 3363 which are explicitly testing Require in modules still to be addressed (to remove from test suite?).
*	Fixing #3896 (incorrect sigma given to printer).	Hugo Herbelin	2015-01-03
\|
*	Fixing #3895 (thanks to PMP for diagnosis).	Hugo Herbelin	2015-01-03
\|
*	An optimization in the use of unification candidates so as to get the	Hugo Herbelin	2015-01-01
\| \| \| \| \| \|	following working: Definition test {A B:Type} {H:A=B} (a:A) : B := rew H in a.
*	Fixing #3892: Ensure that notation variables do not capture names	Hugo Herbelin	2014-12-30
\| \| \| \|	hidden behind another notation.
*	include test-suite/coqchk in the summary log	Enrico Tassi	2014-12-27
\|
*	new test for coqchk	Enrico Tassi	2014-12-26
\|
*	Better doc and a few fixes for Proof using.	Enrico Tassi	2014-12-19
\|
*	Fixing wrong notation level in #3295.	Hugo Herbelin	2014-12-19
\|
*	Proof using: New vernacular to name sets of section variables	Enrico Tassi	2014-12-18
\|
*	Future: blocking by default	Enrico Tassi	2014-12-17
\| \| \| \| \| \|	This makes queries like Print or Extraction block and not raise the error "the value is not ready". This should make CoqIDE work for every kind of script.
*	#3828 is solved.	Hugo Herbelin	2014-12-16
\|
*	Moving #2447 (congruence) to fixed.	Hugo Herbelin	2014-12-16
\|
*	Test for #3654.	Hugo Herbelin	2014-12-16
\|
*	fix bug #2447 in congruence	Pierre Corbineau	2014-12-16
\|
*	Adapted test file for About.	Pierre Courtieu	2014-12-15
\|
*	Tests for #3848 and #3854.	Hugo Herbelin	2014-12-15
\|
*	About now accepts hypothesis names and goal selector.	Pierre Courtieu	2014-12-15
\|
*	Tests for Searchxxx commands added and modified.	Pierre Courtieu	2014-12-15
\|
*	Two fixes in unification (bugs #3782 and #3709)	Matthieu Sozeau	2014-12-12
\| \| \| \| \| \| \| \|	- In evarconv, check_conv_record properly computes the parameters of primitive record projections for later unification, adding env and sigma as arguments. - In unification, backtrack on pattern-unification and not only application unification if eta for a record failed.
*	Test suite: keep message in sync with actual file deletions.	Xavier Clerc	2014-12-11
\|
*	New reproduction cases for the test suite.	Xavier Clerc	2014-12-11
\|
*	Fixing orientation of postponed subtyping problems.	Hugo Herbelin	2014-12-10
\| \| \| \| \| \| \| \| \| \| \|	In the case of conversion, postponing by preserving the initial orientation. Was wrong from its initial version in Jan 2014, but was not visible because evar-evar subtyping was approximated by evar-evar conversion. Thanks to Enrico for a very short example highlighting the problem. In particular, this fixes Ergo.
*	typo	Enrico Tassi	2014-12-10
\|
*	test-suite: few tests for ".v -> .vi -> .vo" compilation chain	Enrico Tassi	2014-12-10
\|
*	Improving evar restriction (this is a risky change, as I remember a	Hugo Herbelin	2014-12-07
\| \| \| \| \| \| \| \|	similar optimization broke at some time some ssreflect code; we now treat the easy case of a let-in to a rel - a pattern common in pattern-matching compilation -; later on, we shall want to investigate whether any let-in found to refer to out of scope rels or vars can be filtered out).
*	Commits on evar-evar unification fixed HoTT_coq_106 and improved the	Hugo Herbelin	2014-12-05
\| \| \| \| \|	status of #3278 (more precisely, it fixed a bug visible in the #3278 report, but a bug which arrived after #3278 was submitted).
*	Take benefit of improved name preservation of evars in e2fa65fcc.	Hugo Herbelin	2014-12-04
\|
*	Updading test-suite.	Hugo Herbelin	2014-12-03
\|
*	When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if	Hugo Herbelin	2014-12-02
\| \| \| \| \| \| \| \| \| \| \|	possible, which is the "natural" way to orient an equation. At least it matters for matching subterms against patterns, so that it is the pattern variables which are substituted if ever the subterm has itself existential variables, as in: Goal exists x, S x = x. eexists. destruct (S _).
*	Fixing test-suite.	Pierre-Marie Pédrot	2014-12-01
\|
*	Adding test for bug #3417.	Pierre-Marie Pédrot	2014-11-30
\|
*	Test for bug #3485.	Pierre-Marie Pédrot	2014-11-30
\|
*	Test for bug #3487.	Pierre-Marie Pédrot	2014-11-30
\|
*	Test of bug #3682.	Pierre-Marie Pédrot	2014-11-30
\|
*	Fix test flags for fake_ide	Enrico Tassi	2014-11-27
\|
*	Bug #3804 is actually closed (thanks to Jason Gross for the notification).	Xavier Clerc	2014-11-25
\|
*	Tweak some test cases.	Xavier Clerc	2014-11-25
\|
*	Adapting to current semantics of "simpl non-evaluable-cst"	Hugo Herbelin	2014-11-25
\|