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

0 files changed, 0 insertions, 0 deletions