Expurgating the useless difference between List0 and List1 at the
level of generic arguments. This only matters at parsing time.

TODO: the current status is not satisfactory enough, as rule
emptyness is still decided w.r.t. generic arguments. This should be
done on a grammar entry basis instead.

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16618 85f007b7-540e-0410-9357-904b9bb8a0f7
Fixing a bug in the native compiler, introduced by r16363, leading to undefined
variables in the generated code.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16619 85f007b7-540e-0410-9357-904b9bb8a0f7
Reorganizing intropatterns: * and ** are not naming intropatterns.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16620 85f007b7-540e-0410-9357-904b9bb8a0f7
Revising r16550 about providing intro patterns for applying injection:
- Introduction of a specific notation for injection intropatterns: [= pats]
- Use of this specific pattern also to apply discriminate on the fly

Note: The automatic injection of dependent tuples over a same first
component (introduced in r10180) still not integrated to the main
parts of injection and its variant (indeed, it applies only for a root
dependent tuple in sigT).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16621 85f007b7-540e-0410-9357-904b9bb8a0f7
Continuing r16621 on injection intro-patterns:
- order of hypothesis was (historically) from right to left in injection but
  already from left to right in decomp_eq, so no need ro fix it there
- made test Injection.v consistent with implementation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16622 85f007b7-540e-0410-9357-904b9bb8a0f7
Added a Register Inline command for the native compiler. Will be ported to the VM
too. Almost only a new grammar entry since the inlining machinery was already
implemented.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16623 85f007b7-540e-0410-9357-904b9bb8a0f7
Pre-create typeclass_instances and rewrite hintdb in Auto

 This way, we avoid relying on the add_auto_init hook. This hook
 is left for the moment, but could probably be removed someday.

 We also stop using create_hint_db, which has an effect on the libstack.
 This wasn't a problem per se, but could if init_summaries is used more
 (for instance to temporary reset coq).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16624 85f007b7-540e-0410-9357-904b9bb8a0f7
Extraction : message about lack of support for toplevel Include

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

 When arguments scopes are set manually, nothing new, they stay
 as they are (until maybe another Arguments invocation).
 But when argument scopes are computed out of the argument type and
 the Bind Scope information, this kind of scope is now dynamic:
 a later Bind Scope will be able to impact the scopes of an earlier
 constant. For Instance:

 Definition f (n:nat) := n.
 About f. (* Argument scope is [nat_scope] *)
 Bind Scope other_scope with nat.
 About f. (* Argument scope is [other_scope] *)

 This allows to get rid of hacks for modifying scopes during functor
 applications. Moreover, the subst_arguments_scope is now
 environment-insensitive (needed for forthcoming changes in declaremods).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16626 85f007b7-540e-0410-9357-904b9bb8a0f7
Lib.contents () instead of Lib.contents_after None

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16628 85f007b7-540e-0410-9357-904b9bb8a0f7
Modops.destr_functor without useless env

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16629 85f007b7-540e-0410-9357-904b9bb8a0f7
Declaremods: major refactoring, stop duplicating libobjects in modules

 When refering to a module / module type, or when doing an include,
 we do not duplicate and substitution original libobjects immediatly.
 Instead, we store the module path, plus a substitution. The libobjects
 are retrieved later from this module path and substituted, typically
 during a Require. This allows to vastly decrease vo size (up to 50%
 on some files in the stdlib). More work is done during load (some
 substitutions), but the extra time overhead appears to be negligible.

 Beware: all subst_function operations should now be
 environment-insensitive, since they may be arbitrarily delayed.
 Apparently only subst_arguments_scope had to be adapted.

 A few more remarks:

 - Increased code factorisation between modules and modtypes
 - Many errors and anomaly are now assert
 - One hack : brutal access of inner parts of module types
   (cf handle_missing_substobjs)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16630 85f007b7-540e-0410-9357-904b9bb8a0f7
"Boolean Equality" and "Case Analysis" are already off by default...

 ... no need to Unset them manually

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16631 85f007b7-540e-0410-9357-904b9bb8a0f7
- Fix uncaught exception NotASort from reductionops, moving decomp_sort to retyping.ml
- In unification's w_merge, assign the evars in the same order they were found. Might
create rare incompatibilities.


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