Remove calls to Global.env and Libobject from Recordops

6 files changed, 79 insertions, 3 deletions

diff --git a/vernac/canonical.ml b/vernac/canonical.ml
new file mode 100644
index 0000000000..92d5731f92
--- /dev/null
+++ b/vernac/canonical.ml
@@ -0,0 +1,39 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \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
+open Libobject
+open Recordops
+
+let open_canonical_structure i (_, o) =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  if Int.equal i 1 then register_canonical_structure env sigma ~warn:false o
+
+let cache_canonical_structure (_, o) =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  register_canonical_structure ~warn:true env sigma o
+
+let discharge_canonical_structure (_,x) = Some x
+
+let inCanonStruc : Constant.t * inductive -> obj =
+  declare_object {(default_object "CANONICAL-STRUCTURE") with
+                  open_function = open_canonical_structure;
+                  cache_function = cache_canonical_structure;
+                  subst_function = (fun (subst,c) -> subst_canonical_structure subst c);
+                  classify_function = (fun x -> Substitute x);
+                  discharge_function = discharge_canonical_structure }
+
+let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
+
+let declare_canonical_structure ref =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  add_canonical_structure (check_and_decompose_canonical_structure env sigma ref)
diff --git a/vernac/canonical.mli b/vernac/canonical.mli
new file mode 100644
index 0000000000..5b223a0615
--- /dev/null
+++ b/vernac/canonical.mli
@@ -0,0 +1,12 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \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
+
+val declare_canonical_structure : GlobRef.t -> unit
diff --git a/vernac/record.ml b/vernac/record.ml
index a7c5318f11..74e5a03659 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -30,6 +30,7 @@ open Constrexpr
 open Constrexpr_ops
 open Goptions
 open Context.Rel.Declaration
+open Libobject
 
 module RelDecl = Context.Rel.Declaration
 
@@ -373,6 +374,27 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f
 
 open Typeclasses
 
+let load_structure i (_, structure) =
+  Recordops.register_structure (Global.env()) structure
+
+let cache_structure o =
+  load_structure 1 o
+
+let subst_structure (subst, (id, kl, projs as obj)) =
+  Recordops.subst_structure subst obj
+
+let discharge_structure (_, x) = Some x
+
+let inStruc : Recordops.struc_tuple -> obj =
+  declare_object {(default_object "STRUCTURE") with
+    cache_function = cache_structure;
+    load_function = load_structure;
+    subst_function = subst_structure;
+    classify_function = (fun x -> Substitute x);
+    discharge_function = discharge_structure }
+
+let declare_structure_entry o =
+  Lib.add_anonymous_leaf (inStruc o)
 
 let declare_structure ~cum finite ubinders univs paramimpls params template ?(kind=StructureComponent) ?name record_data =
   let nparams = List.length params in
@@ -443,7 +465,7 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
     let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
     let build = ConstructRef cstr in
     let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
-    let () = Recordops.declare_structure(cstr, List.rev kinds, List.rev sp_projs) in
+    let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in
     rsp
   in
   List.mapi map record_data
diff --git a/vernac/record.mli b/vernac/record.mli
index 9852840d12..12a2a765b5 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -24,6 +24,8 @@ val declare_projections :
   Constr.rel_context ->
     (Name.t * bool) list * Constant.t option list
 
+val declare_structure_entry : Recordops.struc_tuple -> unit
+
 val definition_structure :
   universe_decl_expr option -> inductive_kind -> template:bool option ->
   Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 3ee785413c..7f5c265eea 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -12,6 +12,7 @@ Vernacextend
 Ppvernac
 Proof_using
 Lemmas
+Canonical
 Class
 Egramcoq
 Metasyntax
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 7ef3777445..a8dfc9cb5a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -572,7 +572,7 @@ let vernac_definition_hook p = function
 | Coercion ->
   Some (Class.add_coercion_hook p)
 | CanonicalStructure ->
-  Some (Lemmas.mk_hook (fun _ _ _ -> Recordops.declare_canonical_structure))
+  Some (Lemmas.mk_hook (fun _ _ _ -> Canonical.declare_canonical_structure))
 | SubClass ->
   Some (Class.add_subclass_hook p)
 | _ -> None
@@ -1041,7 +1041,7 @@ let vernac_require from import qidl =
 (* Coercions and canonical structures *)
 
 let vernac_canonical r =
-  Recordops.declare_canonical_structure (smart_global r)
+  Canonical.declare_canonical_structure (smart_global r)
 
 let vernac_coercion ~atts ref qids qidt =
   let local, polymorphic = Attributes.(parse Notations.(locality ++ polymorphic) atts) in