coq - The formal proof system

Age	Commit message (Collapse)	Author
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

2014-11-25	Adapting to current semantics of "simpl non-evaluable-cst"	Hugo Herbelin

2014-11-25	Experimenting using unification when matching evar/meta free subterms	Hugo Herbelin
	while before these were supposed to consider only syntactically. Made the experiment to unify with all delta flags unset. Keeping the same flags as for non evar/meta free subterms would lead to too much successes, as e.g. "true && b" matching "b" when the modulo_conv_on_closed_terms flag is set, which is the case for rewrite. But maybe should we instead investigate to have the same flags but with the restrict_conv_on_strict_subterms flag set. This rules out examples like "true && b" unifying with "b" and this is another option which is ok for compiling the stdlib without any changes.
2014-11-24	Adding test for bug #3248.	Pierre-Marie Pédrot

2014-11-23	Pass around information on the use of template polymorphism for	Matthieu Sozeau
	inductive types (i.e., ones declared with an explicit anonymous Type at the conclusion of their arity). With this change one can force inductives to live in higher universes even in the non-fully universe polymorphic case (e.g. bug #3821).
2014-11-22	Test for closed #2713 and #2876.	Hugo Herbelin

2014-11-22	Add test-suite file for dependent rewriting example by Vadim Zaliva and	Matthieu Sozeau
	Daniel Schepler.
2014-11-21	Adding test for bug #3326.	Pierre-Marie Pédrot

2014-11-21	Adding test for bug #3424.	Pierre-Marie Pédrot

2014-11-21	Cleaning up closed bugs in test-suite.	Pierre-Marie Pédrot

2014-11-21	Test for bug #3788.	Pierre-Marie Pédrot

2014-11-21	Add test-suite file for bug #3804.	Matthieu Sozeau

2014-11-20	Adding test for bug #3684.	Pierre-Marie Pédrot

2014-11-18	Fixing a little bug with nested but convertible occurrences in "destruct at".	Hugo Herbelin