coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-04-15
\|\
\| *	Test for bug #3199.	Pierre-Marie Pédrot	2015-04-10
\| \|
\| *	Better test-suite files, removing reliance on admit.	Matthieu Sozeau	2015-04-09
\| \|
\| *	Fix declarations of instances to perform restriction of universe	Matthieu Sozeau	2015-04-09
\| \| \| \| \| \| \| \|	instances as definitions and lemmas do (fixes bug# 4121).
\| *	Add test-suite file for bug #4120.	Matthieu Sozeau	2015-04-09
\| \|
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-04-09
\|\\|
\| *	Test for bug #3815.	Pierre-Marie Pédrot	2015-04-06
\| \|
\| *	Fixing test-suite.	Pierre-Marie Pédrot	2015-04-01
\| \|
\| *	Fixing test-suite.	Pierre-Marie Pédrot	2015-03-31
\| \|
* \|	Merge branch 'v8.5' into trunk	Enrico Tassi	2015-03-30
\|\\|
\| *	camlp4: grep away warnings in output/* tests	Enrico Tassi	2015-03-30
\| \|
\| *	Adding test for bug #4165.	Pierre-Marie Pédrot	2015-03-29
\| \|
\| *	Fully fixing bug #3491 (anomaly when building _rect scheme in the	Hugo Herbelin	2015-03-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	presence of let-ins and recursively non-uniform parameters). The bug was in the List.chop of Inductiveops.get_arity which was wrong in the presence of let-ins and recursively non-uniform parameters. The bug #3491 showed up because, in addition to have let-ins, it was wrongly detected as having recursively non-uniform parameters. Also added some comments in declarations.mli.
\| *	Another example about the consequence of a wrong computation of the	Hugo Herbelin	2015-03-25
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	number of recursively uniform parameters in the presence of let-ins. In practice, more recursively non-uniform parameters were assumed and this was used especially for checking positivity of nested types, leading to refusing more nested types than necessary (see Inductive.v).
\| *	Updating test-suite (see previous commit).	Hugo Herbelin	2015-03-24
\| \|
\| *	Fixing computation of non-recursively uniform arguments in the	Hugo Herbelin	2015-03-24
\| \| \| \| \| \| \| \|	presence of let-ins. This fixes #3491.
\| *	Fixing wrong rel_context in checking positivity condition.	Hugo Herbelin	2015-03-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Parameters were missing in the context, apparently without negative effects because the context was used only for whd normalization of types, while reduction (in closure.ml) was resistant to unbound rels. See however next commit for an indirect effect on the wrong computation of non recursively uniform parameters producing an anomaly when computing _rect schemas.
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-23
\|\\|
\| *	Qed export -> Qed exporting	Enrico Tassi	2015-03-22
\| \|
* \|	Merge branch 'v8.5' into trunk	Arnaud Spiwack	2015-03-13
\|\\|
\| *	Add some tests for tryif	Jason Gross	2015-03-13
\| \| \| \| \| \| \| \|	+ adjusting for the removal of `admit` by Arnaud Spiwack.
\| *	Fix regression in HoTT_coq_014.v	Enrico Tassi	2015-03-11
\| \| \| \| \| \| \| \| \| \|	Admitted was not using the partial proof to infer discharged variables. Now it does. The fix makes no sense, but restore the old behavior.
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-11
\|\\|
\| *	admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)	Enrico Tassi	2015-03-11
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- no more inconsistent Axiom in the Prelude - STM can now process Admitted proofs asynchronously - the quick chain can stock "Admitted" jobs in .vio files - the vio2vo step checks the jobs but does not stock the result in the opaque tables (they have no slot) - Admitted emits a warning if the proof is complete - Admitted uses the (partial) proof term to infer section variables used (if not given with Proof using), like for Qed - test-suite: extra line Require TestSuite.admit to each file making use of admit - test-suite/_CoqProject: to pass to CoqIDE and PG the right -Q flag to find TestSuite.admit
\| *	Do not display the status of monomorphic constants unless in ↵	Guillaume Melquiond	2015-03-09
\| \| \| \| \| \| \| \|	universe-polymorphism mode.
\| *	Test for bug #2951.	Pierre-Marie Pédrot	2015-03-08
\| \|
\| *	Test for #4035 (dependent destruction from Ltac).	Hugo Herbelin	2015-03-07
\| \|
* \|	Merge branch 'v8.5' into trunk	Pierre Letouzey	2015-03-06
\|\\|
\| *	Fix testsuite with respect to the new formatting of Fail messages.	Guillaume Melquiond	2015-03-05
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-03-04
\|\\|
\| *	Fix test-suite file, this is open.	Matthieu Sozeau	2015-03-03
\| \|
\| *	Fix bug #3732: firstorder was using detyping to build existential	Matthieu Sozeau	2015-03-03
\| \| \| \| \| \| \| \| \| \| \| \|	instances and forgeting about the evars and universes that could appear there... dirty hack gone, using the evar map properly and avoiding needless constructions/deconstructions of terms.
\| *	Add missing test-suite files and update gitignore.	Matthieu Sozeau	2015-03-03
\| \|
\| *	Add a test-suite file ensuring coinductives with primitive projections	Matthieu Sozeau	2015-03-03
\| \| \| \| \| \| \| \| \| \|	do not enjoy eta-conversion and do not allow the usual failure of subject reduction in presence of dependent pattern-matching.
\| *	Fix test-suite file, this is currently a wontfix, but keep the	Matthieu Sozeau	2015-03-03
\| \| \| \| \| \| \| \|	test-suite file for when we move to a better implementation.
\| *	Fix bug #4103: forgot to allow unfolding projections of cofixpoints like	Matthieu Sozeau	2015-03-03
\| \| \| \| \| \| \| \|	cases, in some cases.
\| *	Fix bug #4101, noccur_evar's expand_projection can legitimately fail	Matthieu Sozeau	2015-03-03
\| \| \| \| \| \| \| \|	when called from w_unify, so we protect it.
\| *	Fix bug #4097.	Matthieu Sozeau	2015-03-02
\| \|
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-02-28
\|\\|
\| *	Adding a test for bug #3612.	Pierre-Marie Pédrot	2015-02-27
\| \|
\| *	Test for bug #3249.	Pierre-Marie Pédrot	2015-02-27
\| \|
\| *	Fix test for #3467, I had moved it in a dumb way.	Maxime Dénès	2015-02-27
\| \|
\| *	Add support so that the type of a match in an inductive type with let-in	Hugo Herbelin	2015-02-27
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	is reduced as if without let-in, when applied to arguments. This allows e.g. to have a head-betazeta-reduced goal in the following example. Inductive Foo : let X := Set in X := I : Foo. Definition foo (x : Foo) : x = x. destruct x. (* or case x, etc. *)
\| *	Fixing first part of bug #3210 (inference of pattern-matching return	Hugo Herbelin	2015-02-27
\| \| \| \| \| \| \| \|	clause in the presence of let-ins in the arity of inductive type).
\| *	Fix test for #3848, still open.	Maxime Dénès	2015-02-27
\| \|
\| *	Moving test for #3467 to closed after PMP's fix.	Maxime Dénès	2015-02-27
\| \|
\| *	Fix test-suite files for bugs #2456 and #3593, still open.	Maxime Dénès	2015-02-27
\| \|
\| *	Add test-suite file for #3649.	Maxime Dénès	2015-02-27
\| \|
\| *	Moving tests for #2456 and #3593 to "opened" until they're fixed.	Maxime Dénès	2015-02-27
\| \|
\| *	Made test for #3392 rely less on unification.	Maxime Dénès	2015-02-27
\| \|