Added a concat function to List theory. Strangely, it was missing.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16633 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing bug #3093 by adding the asked test case.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16634 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing #3089. This implied tweaking the definition of the lexicographic
product of lists, hence possibly introducing incompatibilities.

Parts of the patch by Chantal Keller.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16635 85f007b7-540e-0410-9357-904b9bb8a0f7
Added a way to change dynamically coqtop arguments in CoqIDE.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16636 85f007b7-540e-0410-9357-904b9bb8a0f7
Protecting every call to current_term in CoqIDE so that callback
will not raise an exception if there is no opened tab.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16637 85f007b7-540e-0410-9357-904b9bb8a0f7
Revert "Only arguments declared as implicit can be renamed"

This reverts commit 18a89c271d540d794d44e41f50587bb1cad69802.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16640 85f007b7-540e-0410-9357-904b9bb8a0f7
better error message for unexpected renaming (closes #2987)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16641 85f007b7-540e-0410-9357-904b9bb8a0f7
Tentative fix for #3054: we refresh universes in a term generated
by congruence, as it seems to be done methodically on the remaining
of this plugin.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16642 85f007b7-540e-0410-9357-904b9bb8a0f7
Granting wish #1781:
	Parenthesis matching on click in all term displays.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16643 85f007b7-540e-0410-9357-904b9bb8a0f7