coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Making parentheses mandatory in tactic scopes.	Pierre-Marie Pédrot	2016-03-04
\|
*	Fixing complexity file f_equal.v.	Hugo Herbelin	2015-11-06
\|
*	Fixing complexity issue with f_equal. Thanks to J.-H. Jourdan	Hugo Herbelin	2015-11-06
\| \| \| \| \| \| \|	for reporting it. A "cut" was not appropriately chained on the second goal but on both goals, with the chaining on the first goal introducing noise.
*	Fixing complexity tests for #4076.	Maxime Dénès	2015-02-26
\|
*	Another test for a variant of complexity problem #4076 (thanks to A. Mortberg).	Hugo Herbelin	2015-02-25
\|
*	Compensating 6fd763431 on postponing subtyping evar-evar problems.	Hugo Herbelin	2015-02-23
\| \| \| \| \| \| \|	Pushing pending problems had the side-effect of later solving them in the opposite order as they arrived, resulting on different complexity (see e.g. #4076). We now take care of pushing them in reverse order so that they are treated in the same order.
*	Last test-suite not in Symmetric Patterns syntax	pboutill	2013-01-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16132 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Minor fixes in the test-suite after my recent commits	letouzey	2012-07-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15542 85f007b7-540e-0410-9357-904b9bb8a0f7
*	ZArith + other : favor the use of modern names instead of compat notations	letouzey	2012-07-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- For instance, refl_equal --> eq_refl - Npos, Zpos, Zneg now admit more uniform qualified aliases N.pos, Z.pos, Z.neg. - A new module BinInt.Pos2Z with results about injections from positive to Z - A result about Z.pow pushed in the generic layer - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l} - Using tactic Z.le_elim instead of Zle_lt_or_eq - Some cleanup in ring, field, micromega (use of "Equivalence", "Proper" ...) - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp) - In ZMake and ZMake, functor parameters are now named NN and ZZ instead of N and Z for avoiding confusions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7
*	remove undocumented and scarcely-used tactic auto decomp	letouzey	2012-04-23
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15241 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing format of complexity bug Notations.v.	herbelin	2011-12-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14800 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing amazing loop when using eta-expansion in pattern-matching for	herbelin	2011-12-16
\| \| \| \| \| \| \| \|	printing notations. Since notation printing is not typed, printing "F G" using a notation for "f (fun x => g)" recursively eta-expands G, then x, then a new x and so on forever. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14796 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Optimizing the compilation of unused aliases in pattern-matching.	herbelin	2011-11-21
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14705 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixes in the test-suite after modularisation of ZArith and co	letouzey	2011-05-06
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14114 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed guard check with commutative cuts	barras	2010-05-20
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13022 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Reduced the complexity of evar instantiations from O(n^3) to less than O(n^2).	herbelin	2010-04-19
\| \| \| \| \| \| \| \| \| \| \| \| \| \|	Reasoning modulo variable aliases induced an extra lookup in the environment at each inversion of the components of the evar instances: precomputing the aliases map allowed to gain a factor n. Moreover, solve_evar_evar_l2r was recomputing the evar substitution from the evar instance n more times than needed. Function solve_evar_evar_l2r is still on O(n^2) but it does not seem to be used so often actually. The trivial case has been optimized (linear time) but the general case could probably be also cut down to O(n*log(n)) if needed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12954 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Small things about coqdoc + fixing lettuple.v test (part of bug #2289)	herbelin	2010-03-30
\| \| \| \| \| \| \|	In coqdoc, made links to utf8 notations working and made representation of locations for notations more compact git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12896 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Fixing bug #2279 (printing nested let-in was in exponential time)	herbelin	2010-03-27
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12887 85f007b7-540e-0410-9357-904b9bb8a0f7
*	fixed minor pbs with test cases	barras	2010-03-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12865 85f007b7-540e-0410-9357-904b9bb8a0f7
*	introduced lazy computation of size info in the guard condition	barras	2010-03-11
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12862 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12337 85f007b7-540e-0410-9357-904b9bb8a0f7
*	illegal tactic application was having Ltac interpreter loop	barras	2009-03-04
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11963 85f007b7-540e-0410-9357-904b9bb8a0f7
*	commited complexity test for exponential behavior of unification	barras	2009-02-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11894 85f007b7-540e-0410-9357-904b9bb8a0f7
*	- Optimized "auto decomp" which had a (presumably) exponential in	herbelin	2008-12-26
\| \| \| \| \| \| \| \| \|	the number of conjunctions to split. - A few cleaning and uniformisation in auto.ml. - Removal of v62 hints already in core. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11715 85f007b7-540e-0410-9357-904b9bb8a0f7
*	test-suite/complexity/ring2.v: Zeqb_ok -> Zbool.Zeq_bool_eq	letouzey	2008-07-09
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11216 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Strategy commands are now exported	barras	2008-05-22
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10971 85f007b7-540e-0410-9357-904b9bb8a0f7
*	MAJ et bricoles diverses	herbelin	2008-05-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10923 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un test de complexité de injection (cf bug 1173)	herbelin	2007-04-14
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9769 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Pas de solution à court terme pour ce problème de complexité	herbelin	2007-01-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9548 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Correction petits bugs du check de la test-suite	herbelin	2006-12-28
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9466 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Backtrack sur suppression des vars anonymes des contextes d'evars (echec ↵	herbelin	2006-12-12
\| \| \| \| \| \|	Case15.v et CasesDep.v pas anormal) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9437 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Test bug #932	herbelin	2006-12-12
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9434 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout test setoid_rewrite (cf bug #1176); anglicisation	herbelin	2006-11-01
\| \| \| \|	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9330 85f007b7-540e-0410-9357-904b9bb8a0f7
*	Ajout d'un répertoire de test de la complexité	herbelin	2006-10-06
	git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9222 85f007b7-540e-0410-9357-904b9bb8a0f7