Retroknowledge: use GlobRef.t instead of Constr.t as entry

17 files changed, 83 insertions, 97 deletions

diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 961036d3c5..75cf6b747d 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -659,11 +659,11 @@ let rec lambda_of_constr env c =
 
     (* translation of the argument *)
     let la = lambda_of_constr env a in
-    let entry = mkInd ind in
+    let gr = GlobRef.IndRef ind in
     let la =
       try
         Retroknowledge.get_vm_before_match_info env.global_env.retroknowledge
-          entry la
+          gr la
       with Not_found -> la
     in
     (* translation of the type *)
@@ -721,7 +721,7 @@ and lambda_of_app env f args =
     (try
       (* We delay the compilation of arguments to avoid an exponential behavior *)
       let f = Retroknowledge.get_vm_compiling_info env.global_env.retroknowledge
-          (mkConstU (kn,u)) in
+          (GlobRef.ConstRef kn) in
       let args = lambda_of_args env 0 args in
       f args
     with Not_found ->
@@ -734,6 +734,7 @@ and lambda_of_app env f args =
   | Construct (c,_) ->
     let tag, nparams, arity = Renv.get_construct_info env c in
     let nargs = Array.length args in
+    let gr = GlobRef.ConstructRef c in
     if Int.equal (nparams + arity) nargs then (* fully applied *)
       (* spiwack: *)
       (* 1/ tries to compile the constructor in an optimal way,
@@ -748,7 +749,7 @@ and lambda_of_app env f args =
         try
           Retroknowledge.get_vm_constant_static_info
             env.global_env.retroknowledge
-            f args
+            gr args
         with NotClosed ->
           (* 2/ if the arguments are not all closed (this is
                               expectingly (and it is currently the case) the only
@@ -769,7 +770,7 @@ and lambda_of_app env f args =
           let args = lambda_of_args env nparams rargs in
           Retroknowledge.get_vm_constant_dynamic_info
             env.global_env.retroknowledge
-            f args
+            gr args
       with Not_found ->
         (* 3/ if no special behavior is available, then the compiler
            falls back to the normal behavior *)
@@ -782,7 +783,7 @@ and lambda_of_app env f args =
       (try
          (Retroknowledge.get_vm_constant_dynamic_info
             env.global_env.retroknowledge
-            f) args
+            gr) args
        with Not_found ->
          if nparams <= nargs then (* got all parameters *)
            makeblock tag 0 arity args
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 64c93a2607..62c14f6f07 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -693,12 +693,12 @@ let register_one env field entry =
   { env with retroknowledge = Retroknowledge.add_field env.retroknowledge field entry }
 
 (* [register env field entry] may register several fields when needed *)
-let register env field entry =
+let register env field gr =
   match field with
-    | KInt31 Int31Type ->
-        let i31c = match kind entry with
-                     | Ind i31t -> mkConstructUi (i31t, 1)
-		     | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.")
-	in
-        register_one (register_one env (KInt31 Int31Constructor) i31c) field entry
-    | field -> register_one env field entry
+  | KInt31 Int31Type ->
+    let i31c = match gr with
+      | GlobRef.IndRef i31t -> GlobRef.ConstructRef (i31t, 1)
+      | _ -> anomaly ~label:"Environ.register" (Pp.str "should be an inductive type.")
+    in
+    register_one (register_one env (KInt31 Int31Constructor) i31c) field gr
+  | field -> register_one env field gr
diff --git a/kernel/environ.mli b/kernel/environ.mli
index f45b7be821..1343b9029b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -325,7 +325,7 @@ val retroknowledge : (retroknowledge->'a) -> env -> 'a
 
 val registered : env -> field -> bool
 
-val register : env -> field -> Retroknowledge.entry -> env
+val register : env -> field -> GlobRef.t -> env
 
 (** Native compiler *)
 val no_link_info : link_info
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 98a9973117..9435f46c6b 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -267,7 +267,7 @@ let subst_structure subst = subst_structure subst do_delta_codom
 (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *)
 let add_retroknowledge =
   let perform rkaction env = match rkaction with
-    | Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) ->
+    | Retroknowledge.RKRegister (f, ((GlobRef.ConstRef _ | GlobRef.IndRef _) as e)) ->
       Environ.register env f e
     | _ ->
       CErrors.anomaly ~label:"Modops.add_retroknowledge"
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 122fe95df4..ab40c643f9 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -373,14 +373,14 @@ let is_lazy env prefix t =
   | App (f,args) ->
      begin match kind f with
      | Construct (c,_) ->
-	let entry = mkInd (fst c) in
-	(try
-	    let _ =
-              Retroknowledge.get_native_before_match_info env.retroknowledge
-							  entry prefix c Llazy;
-	    in
+       let gr = GlobRef.IndRef (fst c) in
+       (try
+          let _ =
+            Retroknowledge.get_native_before_match_info env.retroknowledge
+              gr prefix c Llazy;
+          in
 	    false
-	  with Not_found -> true)
+        with Not_found -> true)
      | _ -> true
      end
   | LetIn _ | Case _ | Proj _ -> true
@@ -482,12 +482,12 @@ let rec lambda_of_constr cache env sigma c =
       in
       (* translation of the argument *)
       let la = lambda_of_constr cache env sigma a in
-      let entry = mkInd ind in
+      let gr = GlobRef.IndRef ind in
       let la =
-	try
-          Retroknowledge.get_native_before_match_info (env).retroknowledge
-						      entry prefix (ind,1) la
-	with Not_found -> la
+        try
+         Retroknowledge.get_native_before_match_info (env).retroknowledge
+           gr prefix (ind,1) la
+        with Not_found -> la
       in
       (* translation of the type *)
       let lt = lambda_of_constr cache env sigma t in
@@ -536,7 +536,7 @@ and lambda_of_app cache env sigma f args =
           let prefix = get_const_prefix env kn in
 	  (* We delay the compilation of arguments to avoid an exponential behavior *)
 	  let f = Retroknowledge.get_native_compiling_info
-                    (env).retroknowledge (mkConst kn) prefix in
+                    (env).retroknowledge (GlobRef.ConstRef kn) prefix in
           let args = lambda_of_args cache env sigma 0 args in
 	  f args
       with Not_found ->
@@ -561,17 +561,18 @@ and lambda_of_app cache env sigma f args =
       let expected = nparams + arity in
       let nargs = Array.length args in
       let prefix = get_mind_prefix env (fst (fst c)) in
+      let gr = GlobRef.ConstructRef c in
       if Int.equal nargs expected then 
       try
 	try
 	  Retroknowledge.get_native_constant_static_info
                          (env).retroknowledge
-                         f args
+                         gr args
           with NotClosed ->
 	    assert (Int.equal nparams 0); (* should be fine for int31 *)
             let args = lambda_of_args cache env sigma nparams args in
 	    Retroknowledge.get_native_constant_dynamic_info
-                           (env).retroknowledge f prefix c args
+                           (env).retroknowledge gr prefix c args
         with Not_found ->
           let args = lambda_of_args cache env sigma nparams args in
           makeblock env c u tag args
@@ -579,7 +580,7 @@ and lambda_of_app cache env sigma f args =
         let args = lambda_of_args cache env sigma 0 args in
 	(try
 	    Retroknowledge.get_native_constant_dynamic_info
-              (env).retroknowledge f prefix c args
+              (env).retroknowledge gr prefix c args
 	  with Not_found ->
             mkLapp (Lconstruct (prefix, (c,u))) args)
   | _ -> 
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 2ed846d852..c1a8820bf0 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -19,12 +19,9 @@ open Names
 open Constr
 
 (* The retroknowledge defines a bijective correspondance between some
-   [entry]-s (which are, in fact, merely terms) and [field]-s which
+   [entry]-s (which are, in fact, merely names) and [field]-s which
    are roles assigned to these entries. *)
 
-(* aliased type for clarity purpose*)
-type entry = Constr.t
-
 type int31_field =
   | Int31Bits
   | Int31Type
@@ -95,19 +92,13 @@ type flags = {fastcomputation : bool}
 module Proactive =
   Map.Make (struct type t = field let compare = Pervasives.compare end)
 
-type proactive = entry Proactive.t
+type proactive = GlobRef.t Proactive.t
 
 (* The [reactive] knowledge contains the mapping
    [entry->field]. Fields are later to be interpreted as a
    [reactive_info]. *)
 
-module EntryOrd =
-struct
-  type t = entry
-  let compare = Constr.compare
-end
-
-module Reactive = Map.Make (EntryOrd)
+module Reactive = GlobRef.Map
 
 type reactive_info = {(*information required by the compiler of the VM *)
   vm_compiling :
@@ -154,7 +145,7 @@ and retroknowledge = {flags : flags; proactive : proactive; reactive : reactive}
 (* As per now, there is only the possibility of registering things
    the possibility of unregistering or changing the flag is under study *)
 type action =
-    | RKRegister of field*entry
+    | RKRegister of field * GlobRef.t
 
 
 (*initialisation*)
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index 1436f23739..1fc3cfb817 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.mli
@@ -13,9 +13,6 @@ open Constr
 
 type retroknowledge
 
-(** aliased type for clarity purpose*)
-type entry = Constr.t
-
 (** the following types correspond to the different "things"
    the kernel can learn about.*)
 type int31_field =
@@ -55,7 +52,7 @@ val int31_field_of_string : string -> int31_field
    As per now, there is only the possibility of registering things
    the possibility of unregistering or changing the flag is under study *)
 type action =
-    | RKRegister of field*entry
+    | RKRegister of field * GlobRef.t
 
 
 (** initial value for retroknowledge *)
@@ -66,7 +63,7 @@ val initial_retroknowledge : retroknowledge
    and the continuation cont of the bytecode compilation
    returns the compilation of id in cont if it has a specific treatment
    or raises Not_found if id should be compiled as usual *)
-val get_vm_compiling_info  : retroknowledge -> entry ->
+val get_vm_compiling_info  : retroknowledge -> GlobRef.t ->
                              Cinstr.lambda array -> Cinstr.lambda
 (*Given an identifier id (usually Construct _)
    and its argument array, returns a function that tries an ad-hoc optimisated
@@ -75,7 +72,7 @@ val get_vm_compiling_info  : retroknowledge -> entry ->
    raises Not_found if id should be compiled as usual, and expectingly
    CBytecodes.NotClosed if the term is not a closed constructor pattern
    (a constant for the compiler) *)
-val get_vm_constant_static_info : retroknowledge -> entry ->
+val get_vm_constant_static_info : retroknowledge -> GlobRef.t ->
                                    constr array -> Cinstr.lambda
 
 (*Given an identifier id (usually Construct _ )
@@ -83,45 +80,45 @@ val get_vm_constant_static_info : retroknowledge -> entry ->
    of id+args+cont when id has a specific treatment (in the case of
    31-bit integers, that would be the dynamic compilation into integers)
    or raises Not_found if id should be compiled as usual *)
-val get_vm_constant_dynamic_info : retroknowledge -> entry ->
+val get_vm_constant_dynamic_info : retroknowledge -> GlobRef.t ->
                                    Cinstr.lambda array -> Cinstr.lambda
 
 (** Given a type identifier, this function is used before compiling a match
    over this type. In the case of 31-bit integers for instance, it is used
    to add the instruction sequence which would perform a dynamic decompilation
    in case the argument of the match is not in coq representation *)
-val get_vm_before_match_info : retroknowledge -> entry -> Cinstr.lambda
+val get_vm_before_match_info : retroknowledge -> GlobRef.t -> Cinstr.lambda
                                                        -> Cinstr.lambda
 
 (** Given a type identifier, this function is used by pretyping/vnorm.ml to
    recover the elements of that type from their compiled form if it's non
    standard (it is used (and can be used) only when the compiled form
    is not a block *)
-val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> constr
+val get_vm_decompile_constant_info : retroknowledge -> GlobRef.t -> int -> constr
 
 
-val get_native_compiling_info  : retroknowledge -> entry -> Nativeinstr.prefix ->
+val get_native_compiling_info  : retroknowledge -> GlobRef.t -> Nativeinstr.prefix ->
 				 Nativeinstr.lambda array -> Nativeinstr.lambda
 
-val get_native_constant_static_info : retroknowledge -> entry ->
+val get_native_constant_static_info : retroknowledge -> GlobRef.t ->
                                       constr array -> Nativeinstr.lambda
 
-val get_native_constant_dynamic_info : retroknowledge -> entry ->
+val get_native_constant_dynamic_info : retroknowledge -> GlobRef.t ->
                                        Nativeinstr.prefix -> constructor ->
 				       Nativeinstr.lambda array ->
 				       Nativeinstr.lambda
 
-val get_native_before_match_info : retroknowledge -> entry ->
+val get_native_before_match_info : retroknowledge -> GlobRef.t ->
 				   Nativeinstr.prefix -> constructor ->
 				   Nativeinstr.lambda -> Nativeinstr.lambda
 
 
 (** the following functions are solely used in Environ and Safe_typing to implement
    the functions  register and unregister (and mem) of Environ *)
-val add_field : retroknowledge -> field -> entry -> retroknowledge
+val add_field : retroknowledge -> field -> GlobRef.t -> retroknowledge
 val mem : retroknowledge -> field -> bool
 (* val remove : retroknowledge -> field -> retroknowledge *)
-val find : retroknowledge -> field -> entry
+val find : retroknowledge -> field -> GlobRef.t
 
 
 (** Dispatching type for the above [get_*] functions. *)
@@ -163,4 +160,4 @@ val empty_reactive_info : reactive_info
 
 (** Hook to be set after the compiler are installed to dispatch fields
     into the above [get_*] functions. *)
-val dispatch_hook : (retroknowledge -> entry -> field -> reactive_info) Hook.t
+val dispatch_hook : (retroknowledge -> GlobRef.t -> field -> reactive_info) Hook.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 95eea2d6b0..9d302c69fb 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -977,16 +977,16 @@ let dispatch =
      it to the name of the coq definition in the reactive retroknowledge) *)
   let int31_op n op prim kn =
     { empty_reactive_info with
-      vm_compiling = Some (Clambda.compile_prim n op kn);
-      native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn));
+      vm_compiling = Some (Clambda.compile_prim n op (kn, Univ.Instance.empty)); (*XXX: FIXME universes? *)
+      native_compiling = Some (Nativelambda.compile_prim prim kn);
     }
   in
 
 fun rk value field ->
   (* subfunction which shortens the (very common) dispatch of operations *)
   let int31_op_from_const n op prim =
-    match Constr.kind value with
-      | Constr.Const kn ->  int31_op n op prim kn
+    match value with
+      | GlobRef.ConstRef kn -> int31_op n op prim kn
       | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant.")
   in
   let int31_binop_from_const op prim = int31_op_from_const 2 op prim in
@@ -1002,14 +1002,14 @@ fun rk value field ->
               (Pp.str "add_int31_decompilation_from_type called with an abnormal field.")
         in
         let i31bit_type =
-          match Constr.kind int31bit with
-          | Constr.Ind (i31bit_type,_) -> i31bit_type
+          match int31bit with
+          | GlobRef.IndRef i31bit_type -> i31bit_type
           |  _ -> anomaly ~label:"Environ.register"
               (Pp.str "Int31Bits should be an inductive type.")
         in
         let int31_decompilation =
-          match Constr.kind value with
-          | Constr.Ind (i31t,_) ->
+          match value with
+          | GlobRef.IndRef i31t ->
               constr_of_int31 i31t i31bit_type
           | _ -> anomaly ~label:"Environ.register"
               (Pp.str "should be an inductive type.")
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 2f83e71726..08b97b718e 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -215,7 +215,7 @@ val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a
 [@@ocaml.deprecated "Use the projection of Environ.env"]
 
 val register :
-  field -> Retroknowledge.entry -> safe_transformer0
+  field -> GlobRef.t -> safe_transformer0
 
 val register_inline : Constant.t -> safe_transformer0
 
diff --git a/library/global.mli b/library/global.mli
index 1708976222..6aeae9fd02 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -148,7 +148,7 @@ val universes_of_global : GlobRef.t -> Univ.AUContext.t
 (** {6 Retroknowledge } *)
 
 val register :
-  Retroknowledge.field -> Constr.constr -> unit
+  Retroknowledge.field -> GlobRef.t -> unit
 
 val register_inline : Constant.t -> unit
 
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 9538abcb18..8dad6260ae 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -545,21 +545,6 @@ END
 
 
 (**********************************************************************)
-(*spiwack : Vernac commands for retroknowledge                        *)
-
-VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF
- | [ "Register" constr(c) "as" "int31" pre_ident(n) ] ->
-           [ let env = Global.env () in
-             let evd = Evd.from_env env in
-             let tc,_ctx = Constrintern.interp_constr env evd c in
-             let tc = EConstr.to_constr evd tc in
-             let f = Retroknowledge.(KInt31 (int31_field_of_string n)) in
-             Global.register f tc ]
-END
-
-
-
-(**********************************************************************)
 (* sozeau: abs/gen for induction on instantiated dependent inductives, using "Ford" induction as
   defined by Conor McBride *)
 TACTIC EXTEND generalize_eqs
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 246acfc92e..20185363e6 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -123,7 +123,7 @@ let construct_of_constr_notnative const env tag (mind, _ as ind) u allargs =
   try
     if const then
       let ctyp = type_constructor mind mib u (mip.mind_nf_lc.(0)) params in
-      Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkInd ind) tag, ctyp
+      Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (GlobRef.IndRef ind) tag, ctyp
     else
       raise Not_found
   with Not_found ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 255707dc7b..266e94b34d 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -79,7 +79,7 @@ let construct_of_constr const env tag typ =
   (* spiwack : here be a branch for specific decompilation handled by retroknowledge *)
   try
     if const then
-      ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (mkIndU indu) tag),
+      ((Retroknowledge.get_vm_decompile_constant_info env.retroknowledge (GlobRef.IndRef ind) tag),
        typ) (*spiwack: this may need to be changed in case there are parameters in the
 	               type which may cause a constant value to have an arity.
 	               (type_constructor seems to be all about parameters actually)
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 44c0159d1b..42d9239f36 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -212,8 +212,10 @@ GRAMMAR EXTEND Gram
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> { VernacScheme l }
       | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
 	      l = LIST1 identref SEP "," -> { VernacCombinedScheme (id, l) }
-      | IDENT "Register"; IDENT "Inline"; id = identref ->
-          { VernacRegister(id, RegisterInline) }
+      | IDENT "Register"; g = global; "as"; IDENT "int31"; quid = qualid ->
+          { VernacRegister(g, RegisterRetroknowledge quid) }
+      | IDENT "Register"; IDENT "Inline"; g = global ->
+          { VernacRegister(g, RegisterInline) }
       | IDENT "Universe"; l = LIST1 identref -> { VernacUniverse l }
       | IDENT "Universes"; l = LIST1 identref -> { VernacUniverse l }
       | IDENT "Constraint"; l = LIST1 univ_constraint SEP "," -> { VernacConstraint l }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 63e9e4fe49..9a356bbaef 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1161,7 +1161,11 @@ open Pputils
       | VernacRegister (id, RegisterInline) ->
         return (
           hov 2
-            (keyword "Register Inline" ++ spc() ++ pr_lident id)
+            (keyword "Register Inline" ++ spc() ++ pr_qualid id)
+        )
+      | VernacRegister (id, RegisterRetroknowledge n) ->
+        return (
+          hov 2 (keyword "Register" ++ spc () ++ pr_qualid id ++ spc () ++ keyword "as" ++ str "int31" ++ pr_qualid n)
         )
       | VernacComments l ->
         return (
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index e6b3721134..2b4dfd19a6 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1950,14 +1950,18 @@ let vernac_locate = function
   | LocateOther (s, qid) -> print_located_other s qid
   | LocateFile f -> locate_file f
 
-let vernac_register id r =
+let vernac_register qid r =
+  let gr = Smartlocate.global_with_alias qid in
  if Proof_global.there_are_pending_proofs () then
     user_err Pp.(str "Cannot register a primitive while in proof editing mode.");
-  let kn = Constrintern.global_reference id.v in
-  if not (isConstRef kn) then
-    user_err Pp.(str "Register inline: a constant is expected");
   match r with
-  | RegisterInline -> Global.register_inline (destConstRef kn)
+  | RegisterInline ->
+    if not (isConstRef gr) then
+      user_err Pp.(str "Register inline: a constant is expected");
+    Global.register_inline (destConstRef gr)
+  | RegisterRetroknowledge n ->
+    let f = Retroknowledge.(KInt31 (int31_field_of_string (Libnames.string_of_qualid n))) in
+    Global.register f gr
 
 (********************)
 (* Proof management *)
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 11b2a7d802..ea69ed59a3 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -278,6 +278,7 @@ type extend_name =
    It will be extended with primitive inductive types and operators *)
 type register_kind =
   | RegisterInline
+  | RegisterRetroknowledge of qualid
 
 type bullet = Proof_bullet.t
 [@@ocaml.deprecated "Alias type, please use [Proof_bullet.t]"]
@@ -438,7 +439,7 @@ type nonrec vernac_expr =
   | VernacPrint of printable
   | VernacSearch of searchable * Goal_select.t option * search_restriction
   | VernacLocate of locatable
-  | VernacRegister of lident * register_kind
+  | VernacRegister of qualid * register_kind
   | VernacComments of comment list
 
   (* Proof management *)