coq - The formal proof system

Age	Commit message (Collapse)	Author
2015-01-16	Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"	Matthieu Sozeau
	Not supposed to be part of 8.5beta. This reverts commit 74682bb27da074fedc115238f3085baaccf12d73.
2015-01-13	TCs: Properly handle Hint Extern with conclusions of the form _ -> _	Matthieu Sozeau
	in typeclasses eauto, remaining compatible with eauto and still producing eta-reduced applications for Hint Resolves. Fixes bug #3794.
2015-01-13	Fix test-suite file, we were testing that no anomaly was raised	Matthieu Sozeau
	and this is the case now.
2015-01-12	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-11	Extraction: discard code unnecessary to fulfill a module signature	Pierre Letouzey

2015-01-09	STM: fix handling of side effects in vio2vo	Enrico Tassi

2015-01-06	rename: vi -> vio	Enrico Tassi

2015-01-06	Fixing test for bug #2830.	Pierre-Marie Pédrot

2015-01-05	kernel/ind Change interface of declare_mind and declare_mutual	Matthieu Sozeau
	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.
2015-01-04	Adapting two files from test-suite to now forbidden Require's in modules.	Hugo Herbelin
	Status of 335 and 3363 which are explicitly testing Require in modules still to be addressed (to remove from test suite?).
2015-01-03	Fixing #3896 (incorrect sigma given to printer).	Hugo Herbelin

2015-01-03	Fixing #3895 (thanks to PMP for diagnosis).	Hugo Herbelin

2015-01-01	An optimization in the use of unification candidates so as to get the	Hugo Herbelin
	following working: Definition test {A B:Type} {H:A=B} (a:A) : B := rew H in a.
2014-12-30	Fixing #3892: Ensure that notation variables do not capture names	Hugo Herbelin
	hidden behind another notation.
2014-12-27	include test-suite/coqchk in the summary log	Enrico Tassi

2014-12-26	new test for coqchk	Enrico Tassi

2014-12-19	Better doc and a few fixes for Proof using.	Enrico Tassi

2014-12-19	Fixing wrong notation level in #3295.	Hugo Herbelin

2014-12-18	Proof using: New vernacular to name sets of section variables	Enrico Tassi

2014-12-17	Future: blocking by default	Enrico Tassi
	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.
2014-12-16	#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-15	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-12	Two fixes in unification (bugs #3782 and #3709)	Matthieu Sozeau
	- 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.
2014-12-11	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-10	Fixing orientation of postponed subtyping problems.	Hugo Herbelin
	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.
2014-12-10	typo	Enrico Tassi

2014-12-10	test-suite: few tests for ".v -> .vi -> .vo" compilation chain	Enrico Tassi

2014-12-07	Improving evar restriction (this is a risky change, as I remember a	Hugo Herbelin
	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).
2014-12-05	Commits on evar-evar unification fixed HoTT_coq_106 and improved the	Hugo Herbelin
	status of #3278 (more precisely, it fixed a bug visible in the #3278 report, but a bug which arrived after #3278 was submitted).
2014-12-04	Take benefit of improved name preservation of evars in e2fa65fcc.	Hugo Herbelin

2014-12-03	Updading test-suite.	Hugo Herbelin

2014-12-02	When solving ?id{args} = ?id'{args'}, give preference to ?id:=?id' if	Hugo Herbelin
	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 _).
2014-12-01	Fixing test-suite.	Pierre-Marie Pédrot

2014-11-30	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-27	Fix test flags for fake_ide	Enrico Tassi

2014-11-25	Bug #3804 is actually closed (thanks to Jason Gross for the notification).	Xavier Clerc

2014-11-25	Tweak some test cases.	Xavier Clerc