Added an pattern / occurence syntax for vm_compute.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14951 85f007b7-540e-0410-9357-904b9bb8a0f7
Bug #2041: unfold at betaiotaZETA normalize like unfold

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14952 85f007b7-540e-0410-9357-904b9bb8a0f7
Makefile.build: add targets install-devfiles and install-ide-devfiles

It makes special rules for files useless when the Ocaml used to compile coq is not installed

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14953 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix consequence of pp bugfix in testsuite

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14954 85f007b7-540e-0410-9357-904b9bb8a0f7
index-list.html.template: add missing files

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14955 85f007b7-540e-0410-9357-904b9bb8a0f7
Revert "Tentative to fix bug #2628 by not letting intuition break records. Might be too much of a backwards-incompatible change"
Indeed it is breaking too many scripts.
This reverts commit 47e9afaaa4c08aca97d4f4b5a89cb40da76bd850.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14956 85f007b7-540e-0410-9357-904b9bb8a0f7
Improved synchronisation of stdlib index page with current library state.
- Made generation of index page fail if a file is missing in list or
  listed but unbound in existing theories
- Added a file hidden-files to optionally list library files not to show
  in the index page (though it is currently empty)
- Added directory Unicode (why not to have it after all?)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14957 85f007b7-540e-0410-9357-904b9bb8a0f7
Debugger vs tracer: Two different behaviors wrt printing: The debugger
runs in separate process. It has no access to the global env and it
should not request it. The tracer runs in the same process as Coq and
has full access to the global env and to regular pretty-printing of
global names.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14958 85f007b7-540e-0410-9357-904b9bb8a0f7
Corrected a careless cut-and-paste in Gallina description which dated back to 2003.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14963 85f007b7-540e-0410-9357-904b9bb8a0f7
Fix unblocking code in dependent destruction due to zeta being used in unfold now.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14964 85f007b7-540e-0410-9357-904b9bb8a0f7
More information returned by coqtop about its internal state. Hopefully we'll manage to get rid of the own stack of coqide.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14965 85f007b7-540e-0410-9357-904b9bb8a0f7
correcting inversion in list of generated tcc of Function

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14972 85f007b7-540e-0410-9357-904b9bb8a0f7
A "Grab Existential Variables" to transform the unresolved evars at the end of a proof into goals.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14973 85f007b7-540e-0410-9357-904b9bb8a0f7
Documentation for Grab Existential Variables.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14974 85f007b7-540e-0410-9357-904b9bb8a0f7
Additional comment on Focus Conditions.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14975 85f007b7-540e-0410-9357-904b9bb8a0f7
Arguments supports extra notation scopes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14977 85f007b7-540e-0410-9357-904b9bb8a0f7
- Fix dependency computation in eterm to not consider filtered variables.
- Fix handling of evar map in Program coercion code that could forget some new declarations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14978 85f007b7-540e-0410-9357-904b9bb8a0f7
In [reflexivity], [symmetry] etc, use the type found by looking at the relation as the carrier instead of
the first argument's type (plays nicer with coercions).

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