Now glob_sign and interp_sign only depend on structures defined
upto Genarg, so moved them there. This will allow defining the new
genarg interface.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16584 85f007b7-540e-0410-9357-904b9bb8a0f7
Implementing a new interface for Genarg, with centralized data
structure. The code is quite dumb for now, as it only handles basic
extended generig arguments (ExtraArgTypes). Soon, code from other
modules will be centralized there.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16585 85f007b7-540e-0410-9357-904b9bb8a0f7
Removing the various glob/subst/interp registering functions for
extra argument types and putting them into Genarg.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16586 85f007b7-540e-0410-9357-904b9bb8a0f7
Proof-of-concept: moved four easy-to-handle generic arguments to
their own file, Stdarg.

This required a little trick to correctly handle wit_* naming. We
use a dynamic table to remember exactly where those arguments come
from.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16587 85f007b7-540e-0410-9357-904b9bb8a0f7
KEYID token makes parsing more robust in face of notations

A notation may introduce a new keyword that masks an quasi keyword
(IDENT "of" for example) used in some grammar rules.  KEYID "of"
acepts both "of" as an ident and "of" as a keyword.  Rephrasing grammar
rules with KEYID makes hence them more robust in face of user notations.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16590 85f007b7-540e-0410-9357-904b9bb8a0f7
parse "of" as KEYID "of"

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16591 85f007b7-540e-0410-9357-904b9bb8a0f7
- Keep the refinement of existing evars comming from unification with a rewrite lemma.
- Do an nf_meta before get_type_of in unify_to_type to avoid a possible NotAnArity exception,
raised by type_of_*_knowing_parameters. 


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16592 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing argument extension. Instead of qualified names, string
representing qualified names where interpreted as a whole lowercase
ident.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16593 85f007b7-540e-0410-9357-904b9bb8a0f7
Adding genarg printer to debugger.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16595 85f007b7-540e-0410-9357-904b9bb8a0f7
Revert "parse "of" as KEYID "of""

This reverts commit edb2c43e152d40001616485fcf7fdde5d947f7a2.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16598 85f007b7-540e-0410-9357-904b9bb8a0f7
Revert "KEYID token makes parsing more robust in face of notations"

This reverts commit 950086cd26f83aa8896dde9dc7ef5b3d87307c56.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16599 85f007b7-540e-0410-9357-904b9bb8a0f7
Cutting the dependency of Genarg in constr_expr, glob_constr
related types. This will ultimately allow putting genargs into
these ASTs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16600 85f007b7-540e-0410-9357-904b9bb8a0f7
Splitted up Genarg in four different levels:

1. Genarg itself which only defines the abstract datatypes needed.
2. Genintern, first file of interp/, defining the intern and subst
   functions.
3. Geninterp, first file of tactics/, defining the interp function.
4. Genprint, first file of printing/, dealing with the printers.

The Genarg file has no dependency and is in lib/, so that we can put
generic arguments everywhere, and in particular in ASTs.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7
Generalizing the use of maps instead of lists in the interpretation
of tactics.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16602 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing the semantics of the previous patch.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16603 85f007b7-540e-0410-9357-904b9bb8a0f7
Now, idtac closures use maps instead of association list.

The semantics changed slightly so it may break some scripts, though
it is very unlikely, as they would have to be quite intricated and
poorly written. Indeed, the test-suite passed just fine.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16604 85f007b7-540e-0410-9357-904b9bb8a0f7
Using the whole tactic environment while Pretyping.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16605 85f007b7-540e-0410-9357-904b9bb8a0f7
Cleaning up the type of Tacinterp.extract_ltac_constr_values.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16606 85f007b7-540e-0410-9357-904b9bb8a0f7
Useless use of maps in constr internalizing.

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