[states] Move States to vernac

We continue to push state layers upwards, in preparation of a
functional vernacular interpretation.

Now we move `States` and `Printmod` which messes with the global
state as to temporarily create envs with modules.

5 files changed, 551 insertions, 0 deletions

diff --git a/vernac/printmod.ml b/vernac/printmod.ml
new file mode 100644
index 0000000000..9beac17546
--- /dev/null
+++ b/vernac/printmod.ml
@@ -0,0 +1,458 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Util
+open Constr
+open Context
+open Pp
+open Names
+open Environ
+open Declarations
+open Libnames
+open Goptions
+
+(** Note: there is currently two modes for printing modules.
+    - The "short" one, that just prints the names of the fields.
+    - The "rich" one, that also tries to print the types of the fields.
+    The short version used to be the default behavior, but now we print
+    types by default. The following option allows changing this.
+*)
+
+module Tag =
+struct
+
+  let definition = "module.definition"
+  let keyword    = "module.keyword"
+
+end
+
+let tag t s = Pp.tag t s
+let tag_definition s = tag Tag.definition s
+let tag_keyword s = tag Tag.keyword s
+
+type short = OnlyNames | WithContents
+
+let short = ref false
+
+let () =
+  declare_bool_option
+    { optdepr  = false;
+      optkey   = ["Short";"Module";"Printing"];
+      optread  = (fun () -> !short) ;
+      optwrite = ((:=) short) }
+
+(** Each time we have to print a non-globally visible structure,
+    we place its elements in a fake fresh namespace. *)
+
+let mk_fake_top =
+  let r = ref 0 in
+  fun () -> incr r; Id.of_string ("FAKETOP"^(string_of_int !r))
+
+let def s = tag_definition (str s)
+let keyword s = tag_keyword (str s)
+
+let get_new_id locals id =
+  let rec get_id l id =
+    let dir = DirPath.make [id] in
+      if not (Nametab.exists_dir dir) then
+        id
+      else
+        get_id (Id.Set.add id l) (Namegen.next_ident_away id l)
+  in
+  let avoid = List.fold_left (fun accu (_, id) -> Id.Set.add id accu) Id.Set.empty locals in
+    get_id avoid id
+
+(** Inductive declarations *)
+
+open Reduction
+
+let print_params env sigma params =
+  if List.is_empty params then mt ()
+  else Printer.pr_rel_context env sigma params ++ brk(1,2)
+
+let print_constructors envpar sigma names types =
+  let pc =
+    prlist_with_sep (fun () -> brk(1,0) ++ str "| ")
+      (fun (id,c) -> Id.print id ++ str " : " ++ Printer.pr_lconstr_env envpar sigma c)
+      (Array.to_list (Array.map2 (fun n t -> (n,t)) names types))
+  in
+  hv 0 (str "  " ++ pc)
+
+let build_ind_type mip =
+  Inductive.type_of_inductive mip
+
+let print_one_inductive env sigma mib ((_,i) as ind) =
+  let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
+  let mip = mib.mind_packets.(i) in
+  let params = Inductive.inductive_paramdecls (mib,u) in
+  let nparamdecls = Context.Rel.length params in
+  let args = Context.Rel.to_extended_list mkRel 0 params in
+  let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type ((mib,mip),u)) args in
+  let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
+  let cstrtypes = Array.map (fun c -> hnf_prod_applist_assum env nparamdecls c args) cstrtypes in
+  let envpar = push_rel_context params env in
+  let inst =
+    if Declareops.inductive_is_polymorphic mib then
+      Printer.pr_universe_instance sigma u
+    else mt ()
+  in
+  hov 0 (
+    Id.print mip.mind_typename ++ inst ++ brk(1,4) ++ print_params env sigma params ++
+    str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++
+  brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes
+
+let print_mutual_inductive env mind mib udecl =
+  let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x))
+  in
+  let keyword =
+    let open Declarations in
+    match mib.mind_finite with
+    | Finite -> "Inductive"
+    | BiFinite -> "Variant"
+    | CoFinite -> "CoInductive"
+  in
+  let bl = Printer.universe_binders_with_opt_names
+      (Declareops.inductive_polymorphic_context mib) udecl
+  in
+  let sigma = Evd.from_ctx (UState.of_binders bl) in
+  hov 0 (def keyword ++ spc () ++
+         prlist_with_sep (fun () -> fnl () ++ str"  with ")
+           (print_one_inductive env sigma mib) inds ++
+         Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes)
+
+let get_fields =
+  let rec prodec_rec l subst c =
+    match kind c with
+    | Prod (na,t,c) ->
+        let id = match na.binder_name with Name id -> id | Anonymous -> Id.of_string "_" in
+        prodec_rec ((id,true,Vars.substl subst t)::l) (mkVar id::subst) c
+    | LetIn (na,b,_,c) ->
+        let id = match na.binder_name with Name id -> id | Anonymous -> Id.of_string "_" in
+        prodec_rec ((id,false,Vars.substl subst b)::l) (mkVar id::subst) c
+    | _               -> List.rev l
+  in
+  prodec_rec [] []
+
+let print_record env mind mib udecl =
+  let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
+  let mip = mib.mind_packets.(0) in
+  let params = Inductive.inductive_paramdecls (mib,u) in
+  let nparamdecls = Context.Rel.length params in
+  let args = Context.Rel.to_extended_list mkRel 0 params in
+  let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type ((mib,mip),u)) args in
+  let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
+  let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
+  let fields = get_fields cstrtype in
+  let envpar = push_rel_context params env in
+  let bl = Printer.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib)
+      udecl
+  in
+  let sigma = Evd.from_ctx (UState.of_binders bl) in
+  let keyword =
+    let open Declarations in
+    match mib.mind_finite with
+    | BiFinite -> "Record"
+    | Finite -> "Inductive"
+    | CoFinite -> "CoInductive"
+  in
+  hov 0 (
+    hov 0 (
+      def keyword ++ spc () ++ Id.print mip.mind_typename ++ brk(1,4) ++
+      print_params env sigma params ++
+      str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++
+      str ":= " ++ Id.print mip.mind_consnames.(0)) ++
+    brk(1,2) ++
+    hv 2 (str "{ " ++
+      prlist_with_sep (fun () -> str ";" ++ brk(2,0))
+        (fun (id,b,c) ->
+          Id.print id ++ str (if b then " : " else " := ") ++
+          Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++
+    Printer.pr_universes sigma ?variance:mib.mind_variance mib.mind_universes
+  )
+
+let pr_mutual_inductive_body env mind mib udecl =
+  if mib.mind_record != NotRecord && not !Flags.raw_print then
+    print_record env mind mib udecl
+  else
+    print_mutual_inductive env mind mib udecl
+
+(** Modpaths *)
+
+let rec print_local_modpath locals = function
+  | MPbound mbid -> Id.print (Util.List.assoc_f MBId.equal mbid locals)
+  | MPdot(mp,l) ->
+      print_local_modpath locals mp ++ str "." ++ Label.print l
+  | MPfile _ -> raise Not_found
+
+let print_modpath locals mp =
+  try (* must be with let because streams are lazy! *)
+    let qid = Nametab.shortest_qualid_of_module mp in
+      pr_qualid qid
+  with
+    | Not_found -> print_local_modpath locals mp
+
+let print_kn locals kn =
+  try
+    let qid = Nametab.shortest_qualid_of_modtype kn in
+      pr_qualid qid
+  with
+      Not_found ->
+        try
+          print_local_modpath locals kn
+        with
+            Not_found -> print_modpath locals kn
+
+let nametab_register_dir obj_mp =
+  let id = mk_fake_top () in
+  let obj_dir = DirPath.make [id] in
+  Nametab.(push_dir (Until 1) obj_dir (GlobDirRef.DirModule { obj_dir; obj_mp; }))
+
+(** Nota: the [global_reference] we register in the nametab below
+    might differ from internal ones, since we cannot recreate here
+    the canonical part of constant and inductive names, but only
+    the user names. This works nonetheless since we search now
+    [Nametab.the_globrevtab] modulo user name. *)
+
+let nametab_register_body mp dir (l,body) =
+  let push id ref =
+    Nametab.push (Nametab.Until (1+List.length (DirPath.repr dir)))
+      (make_path dir id) ref
+  in
+  match body with
+    | SFBmodule _ -> () (* TODO *)
+    | SFBmodtype _ -> () (* TODO *)
+    | SFBconst _ ->
+      push (Label.to_id l) (GlobRef.ConstRef (Constant.make2 mp l))
+    | SFBmind mib ->
+      let mind = MutInd.make2 mp l in
+      Array.iteri
+        (fun i mip ->
+          push mip.mind_typename (GlobRef.IndRef (mind,i));
+          Array.iteri (fun j id -> push id (GlobRef.ConstructRef ((mind,i),j+1)))
+            mip.mind_consnames)
+        mib.mind_packets
+
+type mod_ops =
+  { import_module : export:bool -> ModPath.t -> unit
+  ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit
+  }
+
+let nametab_register_module_body ~mod_ops mp struc =
+  (* If [mp] is a globally visible module, we simply import it *)
+  try mod_ops.import_module ~export:false mp
+  with Not_found ->
+    (* Otherwise we try to emulate an import by playing with nametab *)
+    nametab_register_dir mp;
+    List.iter (nametab_register_body mp DirPath.empty) struc
+
+let get_typ_expr_alg mtb = match mtb.mod_type_alg with
+  | Some (NoFunctor me) -> me
+  | _ -> raise Not_found
+
+let nametab_register_modparam ~mod_ops mbid mtb =
+  let id = MBId.to_id mbid in
+  match mtb.mod_type with
+  | MoreFunctor _ -> id (* functorial param : nothing to register *)
+  | NoFunctor struc ->
+    (* We first try to use the algebraic type expression if any,
+       via a Declaremods function that converts back to module entries *)
+    try
+      let () = mod_ops.process_module_binding mbid (get_typ_expr_alg mtb) in
+      id
+    with e when CErrors.noncritical e ->
+      (* Otherwise, we try to play with the nametab ourselves *)
+      let mp = MPbound mbid in
+      let check id = Nametab.exists_dir (DirPath.make [id]) in
+      let id = Namegen.next_ident_away_from id check in
+      let dir = DirPath.make [id] in
+      nametab_register_dir mp;
+      List.iter (nametab_register_body mp dir) struc;
+      id
+
+let print_body is_impl extent env mp (l,body) =
+  let name = Label.print l in
+  hov 2 (match body with
+    | SFBmodule _ -> keyword "Module" ++ spc () ++ name
+    | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name
+    | SFBconst cb ->
+       let ctx = Declareops.constant_polymorphic_context cb in
+      (match cb.const_body with
+        | Def _ -> def "Definition" ++ spc ()
+        | OpaqueDef _ when is_impl -> def "Theorem" ++ spc ()
+        | _ -> def "Parameter" ++ spc ()) ++ name ++
+      (match extent with
+         | OnlyNames -> mt ()
+         | WithContents ->
+            let bl = Printer.universe_binders_with_opt_names ctx None in
+            let sigma = Evd.from_ctx (UState.of_binders bl) in
+            str " :" ++ spc () ++
+            hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++
+            (match cb.const_body with
+              | Def l when is_impl ->
+                spc () ++
+                hov 2 (str ":= " ++
+                       Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l))
+              | _ -> mt ()) ++ str "." ++
+            Printer.pr_abstract_universe_ctx sigma ctx)
+    | SFBmind mib ->
+      match extent with
+      | WithContents ->
+        pr_mutual_inductive_body env (MutInd.make2 mp l) mib None
+      | OnlyNames ->
+        let keyword =
+          let open Declarations in
+          match mib.mind_finite with
+          | Finite -> def "Inductive"
+          | BiFinite -> def "Variant"
+          | CoFinite -> def "CoInductive"
+        in
+        keyword ++ spc () ++ name)
+
+let print_struct is_impl extent env mp struc =
+  prlist_with_sep spc (print_body is_impl extent env mp) struc
+
+let print_structure ~mod_ops is_type extent env mp locals struc =
+  let env' = Modops.add_structure mp struc Mod_subst.empty_delta_resolver env in
+  nametab_register_module_body ~mod_ops mp struc;
+  let kwd = if is_type then "Sig" else "Struct" in
+  hv 2 (keyword kwd ++ spc () ++ print_struct false extent env' mp struc ++
+        brk (1,-2) ++ keyword "End")
+
+let rec flatten_app mexpr l = match mexpr with
+  | MEapply (mexpr, arg) -> flatten_app mexpr (arg::l)
+  | MEident mp -> mp::l
+  | MEwith _ -> assert false
+
+let rec print_typ_expr extent env mp locals mty =
+  match mty with
+  | MEident kn -> print_kn locals kn
+  | MEapply _ ->
+      let lapp = flatten_app mty [] in
+      let fapp = List.hd lapp in
+      let mapp = List.tl lapp in
+      hov 3 (str"(" ++ (print_kn locals fapp) ++ spc () ++
+                 prlist_with_sep spc (print_modpath locals) mapp ++ str")")
+  | MEwith(me,WithDef(idl,(c, _)))->
+      let s = String.concat "." (List.map Id.to_string idl) in
+      let body = match extent with
+        | WithContents ->
+            let sigma = Evd.from_env env in
+            spc() ++ str ":=" ++ spc() ++ Printer.pr_lconstr_env env sigma c
+        | OnlyNames ->
+            mt() in
+      hov 2 (print_typ_expr extent env mp locals me ++ spc() ++ str "with" ++ spc()
+             ++ def "Definition"++ spc() ++ str s ++ body)
+  | MEwith(me,WithMod(idl,mp'))->
+      let s = String.concat "." (List.map Id.to_string idl) in
+      let body = match extent with
+        | WithContents ->
+            spc() ++ str ":="++ spc() ++ print_modpath locals mp'
+        | OnlyNames -> mt () in
+      hov 2 (print_typ_expr extent env mp locals me ++ spc() ++ str "with" ++ spc() ++
+             keyword "Module"++ spc() ++ str s ++ body)
+
+let print_mod_expr env mp locals = function
+  | MEident mp -> print_modpath locals mp
+  | MEapply _ as me ->
+      let lapp = flatten_app me [] in
+      hov 3
+        (str"(" ++ prlist_with_sep spc (print_modpath locals) lapp ++ str")")
+  | MEwith _ -> assert false (* No 'with' syntax for modules *)
+
+let rec print_functor ~mod_ops fty fatom is_type extent env mp locals = function
+  | NoFunctor me -> fatom ~mod_ops is_type extent env mp locals me
+  | MoreFunctor (mbid,mtb1,me2) ->
+      let id = nametab_register_modparam ~mod_ops mbid mtb1 in
+      let mp1 = MPbound mbid in
+      let pr_mtb1 = fty ~mod_ops extent env mp1 locals mtb1 in
+      let env' = Modops.add_module_type mp1 mtb1 env in
+      let locals' = (mbid, get_new_id locals (MBId.to_id mbid))::locals in
+      let kwd = if is_type then "Funsig" else "Functor" in
+      hov 2
+        (keyword kwd ++ spc () ++
+         str "(" ++ Id.print id ++ str ":" ++ pr_mtb1 ++ str ")" ++
+         spc() ++ print_functor ~mod_ops fty fatom is_type extent env' mp locals' me2)
+
+let rec print_expression ~mod_ops x =
+  print_functor ~mod_ops
+    print_modtype
+    (fun ~mod_ops -> function true -> print_typ_expr | false -> fun _ -> print_mod_expr) x
+
+and print_signature ~mod_ops x =
+  print_functor ~mod_ops print_modtype print_structure x
+
+and print_modtype ~mod_ops extent env mp locals mtb = match mtb.mod_type_alg with
+  | Some me -> print_expression ~mod_ops true extent env mp locals me
+  | None -> print_signature ~mod_ops true extent env mp locals mtb.mod_type
+
+let rec printable_body dir =
+  let dir = pop_dirpath dir in
+    DirPath.is_empty dir ||
+    try
+      let open Nametab.GlobDirRef in
+      match Nametab.locate_dir (qualid_of_dirpath dir) with
+          DirOpenModtype _ -> false
+        | DirModule _ | DirOpenModule _ -> printable_body dir
+        | _ -> true
+    with
+        Not_found -> true
+
+(** Since we might play with nametab above, we should reset to prior
+    state after the printing *)
+
+let print_expression' ~mod_ops is_type extent env mp me =
+  States.with_state_protection
+    (fun e -> print_expression ~mod_ops is_type extent env mp [] e) me
+
+let print_signature' ~mod_ops is_type extent env mp me =
+  States.with_state_protection
+    (fun e -> print_signature ~mod_ops is_type extent env mp [] e) me
+
+let unsafe_print_module ~mod_ops extent env mp with_body mb =
+  let name = print_modpath [] mp in
+  let pr_equals = spc () ++ str ":= " in
+  let body = match with_body, mb.mod_expr with
+    | false, _
+    | true, Abstract -> mt()
+    | _, Algebraic me -> pr_equals ++ print_expression' ~mod_ops false extent env mp me
+    | _, Struct sign -> pr_equals ++ print_signature' ~mod_ops false extent env mp sign
+    | _, FullStruct -> pr_equals ++ print_signature' ~mod_ops false extent env mp mb.mod_type
+  in
+  let modtype = match mb.mod_expr, mb.mod_type_alg with
+    | FullStruct, _ -> mt ()
+    | _, Some ty -> brk (1,1) ++ str": " ++ print_expression' ~mod_ops true extent env mp ty
+    | _, _ -> brk (1,1) ++ str": " ++ print_signature' ~mod_ops true extent env mp mb.mod_type
+  in
+  hv 0 (keyword "Module" ++ spc () ++ name ++ modtype ++ body)
+
+exception ShortPrinting
+
+let print_module ~mod_ops with_body mp =
+  let me = Global.lookup_module mp in
+  try
+    if !short then raise ShortPrinting;
+    unsafe_print_module ~mod_ops WithContents
+      (Global.env ()) mp with_body me ++ fnl ()
+  with e when CErrors.noncritical e ->
+    unsafe_print_module ~mod_ops OnlyNames
+      (Global.env ()) mp with_body me ++ fnl ()
+
+let print_modtype ~mod_ops kn =
+  let mtb = Global.lookup_modtype kn in
+  let name = print_kn [] kn in
+  hv 1
+    (keyword "Module Type" ++ spc () ++ name ++ str " =" ++ spc () ++
+     try
+      if !short then raise ShortPrinting;
+      print_signature' ~mod_ops true WithContents
+        (Global.env ()) kn mtb.mod_type
+     with e when CErrors.noncritical e ->
+      print_signature' ~mod_ops true OnlyNames
+        (Global.env ()) kn mtb.mod_type)
diff --git a/vernac/printmod.mli b/vernac/printmod.mli
new file mode 100644
index 0000000000..c7f056063b
--- /dev/null
+++ b/vernac/printmod.mli
@@ -0,0 +1,26 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+(** false iff the module is an element of an open module type *)
+val printable_body : DirPath.t -> bool
+
+val pr_mutual_inductive_body : Environ.env ->
+  MutInd.t -> Declarations.mutual_inductive_body ->
+  UnivNames.univ_name_list option -> Pp.t
+
+type mod_ops =
+  { import_module : export:bool -> ModPath.t -> unit
+  ; process_module_binding : MBId.t -> Declarations.module_alg_expr -> unit
+  }
+
+val print_module : mod_ops:mod_ops -> bool -> ModPath.t -> Pp.t
+val print_modtype : mod_ops:mod_ops -> ModPath.t -> Pp.t
diff --git a/vernac/states.ml b/vernac/states.ml
new file mode 100644
index 0000000000..b6904263df
--- /dev/null
+++ b/vernac/states.ml
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+type state = Lib.frozen * Summary.frozen
+
+let lib_of_state = fst
+let summary_of_state = snd
+let replace_summary (lib,_) st = lib, st
+let replace_lib (_,st) lib = lib, st
+
+let freeze ~marshallable =
+  (Lib.freeze (), Summary.freeze_summaries ~marshallable)
+
+let unfreeze (fl,fs) =
+  Lib.unfreeze fl;
+  Summary.unfreeze_summaries fs
+
+(* Rollback. *)
+
+let with_state_protection f x =
+  let st = freeze ~marshallable:false in
+  try
+    let a = f x in unfreeze st; a
+  with reraise ->
+    let reraise = Exninfo.capture reraise in
+    (unfreeze st; Exninfo.iraise reraise)
diff --git a/vernac/states.mli b/vernac/states.mli
new file mode 100644
index 0000000000..51db83ca03
--- /dev/null
+++ b/vernac/states.mli
@@ -0,0 +1,32 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(** {6 States of the system} *)
+
+(** In that module, we provide functions to get
+  and set the state of the whole system. Internally, it is done by
+  freezing the states of both [Lib] and [Summary]. We provide functions
+  to write and restore state to and from a given file. *)
+
+type state
+val freeze : marshallable:bool -> state
+val unfreeze : state -> unit
+
+val summary_of_state : state -> Summary.frozen
+val lib_of_state : state -> Lib.frozen
+val replace_summary : state -> Summary.frozen -> state
+val replace_lib : state -> Lib.frozen -> state
+
+(** {6 Rollback } *)
+
+(** [with_state_protection f x] applies [f] to [x] and restores the
+  state of the whole system as it was before applying [f] *)
+
+val with_state_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 23dde0dd29..085e2e35bc 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -1,6 +1,8 @@
 Vernacexpr
 Attributes
 Pvernac
+States
+Printmod
 Declaremods
 G_vernac
 G_proofs