Repair coqcheck : constant_body constraints are also future

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16706 85f007b7-540e-0410-9357-904b9bb8a0f7
Attempt to restore hash-consing of opaque terms

 Without this, the stdlib vo files are +30% larger

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

 - No more modinfo sub-record in the safe_environment record,
   this was a syntactic pain.
     senv.modinfo.modpath --> senv.modpath
     senv.modinfo.variant --> senv.modvariant
     senv.modinfo.resolver --> senv.modresolver
     senv.modinfo.resolver_of_param --> senv.paramresolver
     senv.modinfo.label : removed (can be inferred from modpath)

 - No more systematic chaining of safe_environment ('old' field).
   Instead, earlier safe_environment is stored in the modvariant field
   when necessary (STRUCT and SIG case).

 - Improved sharing between end_module and end_modtype

 - More qualified names instead of open, better comments, ...

 - Some user errors are now checked earlier elsewhere (see for
   instance vernac_end_segment), so we can turn these errors into
   asserts. The user error about higher-order include is now algebraic.

 - Highlight the idea of a state monad in Safe_typing :
   type 'a safe_transformer = safe_environment -> 'a * safe_environment
   More systematic code in Global, thanks to 'globalize' function.

 - Declaremods : less informations stored in openmod_info

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

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16709 85f007b7-540e-0410-9357-904b9bb8a0f7
Himsg : strict 80-column indentation

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16710 85f007b7-540e-0410-9357-904b9bb8a0f7
Declareops + Modops : more clever substitutions

 We try harder to preserve pointer equality when substituting.
 This will probably have little effect (for instance the
 constr_substituted are anyway _never_ substituted in place),
 but it cannot harm.

 Two particular cases:
 - we try to share (and maintain shared) mind_user_lc and mind_nf_lc
 - we try to share (and maintain shared) mod_expr and mod_type

 TODO: check that native compiler is still ok, since we might have
 less (ref NotLinked) now. Having references in constant_body and co
 is anyway a Very Bad Idea (TM).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16711 85f007b7-540e-0410-9357-904b9bb8a0f7
Declarations.mli: reorganization of modular structures

 The earlier type [struct_expr_body] was far too broad,
 leading to code with unclear invariants, many "assert false", etc etc.
 Its replacement [module_alg_expr] has only three constructors:
   * MEident
   * MEapply : note the module_path as 2nd arg, no more constraints here
   * MEwith : no more constant_body inside, constr is just fine
 But no more SEBfunctor or SEBstruct constructor here (see below).
 This way, this datatype corresponds to algebraic expressions,
 i.e. anything that can appear in non-interactive modules.
 In fact, it even coincides now with [Entries.module_struct_entry].

 - Functor constructors are now necessarily on top of other
   structures thanks to a generic [functorize] datatype.

 - Structures are now separated from algebraic expressions by design :
   the [mod_type] and [typ_expr] fields now only contain structures
   (or functorized structures), while [mod_type_alg] and [typ_expr_alg]
   are restricted to algebraic expressions only.

 - Only the implementation field [mod_expr] could be either algebraic
   or structural. We handle this via a specialized datatype
   [module_implementation] with four constructors:

    * Abstract : no implementation (cf. for instance Declare Module)
    * Algebraic(_) : for non-interactive modules, e.g. Module M := N.
    * Struct(_) : for interactive module, e.g. Module M : T. ... End M.
    * FullStruct : for interactive module with no type restriction.

   The [FullStruct] is a particular case of [Struct] where the implementation
   need not be stored at all, since it is exactly equal to its expanded
   type present in [mod_type]. This is less fragile than hoping as earlier
   that pointer equality between [mod_type] and [mod_expr] will be
   preserved...

 - We clearly emphasize that only [mod_type] and [typ_expr] are
   relevant for the kernel, while [mod_type_alg] and [typ_expr_alg]
   are there only for a nicer extraction and shorter module printing.
   [mod_expr] is also not accessed by the kernel, but it is important
   for Print Assumptions later.

 - A few implicit invariants remain, for instance "no MEwith in mod_expr",
   see the final comment in Declarations

 - Heavy refactoring of module-related files : modops, mod_typing,
   safe_typing, declaremods, extraction/extract_env.ml ...

 - Coqchk has been adapted accordingly. The code concerning MEwith
   in Mod_checking is now gone, since we cannot have any in mod_expr.

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