Modules and ppvernac, sequel of Enrico's commit 16261

 After some investigation, I see no reason to try to hack
 the nametab in ppvernac, since everything happens there
 at a lower level (constr_expr). So the offending code that
 Enrico protected with a State.with_state_protection is now gone.

 By the way, moved some types from Declaremods to Vernacexpr
 to avoid some dependencies

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

3 files changed, 13 insertions, 6 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 915ab9d4c5..640bd0b08d 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -343,6 +343,9 @@ let context l =
       in
       let impl = List.exists test impls in
       let decl = (Discharge, Definitional) in
-      let nstatus = Command.declare_assumption false decl t [] impl None (Loc.ghost, id) in
+      let nstatus =
+        Command.declare_assumption false decl t [] impl
+          Vernacexpr.NoInline (Loc.ghost, id)
+      in
       status && nstatus
   in List.fold_left fn true (List.rev ctx)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 0b2e6b352f..f8230d63d2 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -34,6 +34,7 @@ open Evarutil
 open Evarconv
 open Indschemes
 open Misctypes
+open Vernacexpr
 
 let rec under_binders env f n c =
   if Int.equal n 0 then f env Evd.empty c else
@@ -188,7 +189,12 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = match loca
   true
 | Global | Local | Discharge ->
   let local = get_locality ident local in
-  let decl = (ParameterEntry (None,c,nl), IsAssumption kind) in
+  let inl = match nl with
+    | NoInline -> None
+    | DefaultInline -> Some (Flags.get_inline_level())
+    | InlineAt i -> Some i
+  in
+  let decl = (ParameterEntry (None,c,inl), IsAssumption kind) in
   let kn = declare_constant ident ~local decl in
   let gr = ConstRef kn in
   let () = maybe_declare_manual_implicits false gr imps in
@@ -386,8 +392,6 @@ let declare_mutual_inductive_with_eliminations isrecord mie impls =
   declare_default_schemes mind;
   mind
 
-open Vernacexpr
-
 type one_inductive_impls =
   Impargs.manual_explicitation list (* for inds *)*
   Impargs.manual_explicitation list list (* for constrs *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index eb0eef38f5..08151c859e 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -51,11 +51,11 @@ val interp_assumption :
     nor in a module type and meant to be instantiated. *)
 val declare_assumption : coercion_flag -> assumption_kind -> types ->
   Impargs.manual_implicits ->
-  bool (** implicit *) -> Entries.inline -> variable Loc.located -> bool
+  bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located -> bool
 
 val declare_assumptions : variable Loc.located list ->
   coercion_flag -> assumption_kind -> types -> Impargs.manual_implicits ->
-  bool -> Entries.inline -> bool
+  bool -> Vernacexpr.inline -> bool
 
 (** {6 Inductive and coinductive types} *)