When doing setoid_rewrite through rewrite, do resolution of classes
in w_unify_to_subterm, deactivated by previous patch (fixes RelationAlgebra).


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16579 85f007b7-540e-0410-9357-904b9bb8a0f7
Using an "extra" Store.t field in interp_sign instead of dedicated
record fields.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16580 85f007b7-540e-0410-9357-904b9bb8a0f7
Exporting field f_debug (needed for Ssreflect).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16581 85f007b7-540e-0410-9357-904b9bb8a0f7
Documenting a potential source of incompleteness in the ring tactic,
when reification is customized with a user-defined set of coefficients.



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16583 85f007b7-540e-0410-9357-904b9bb8a0f7
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