1 files changed, 70 insertions, 6 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index dec9e1deb8..a5f81d1e59 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -43,7 +43,6 @@ type key = int CEphemeron.key option ref
 
 type link_info =
   | Linked of string
-  | LinkedInteractive of string
   | NotLinked
 
 type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key)
@@ -104,7 +103,6 @@ type env = {
   env_typing_flags  : typing_flags;
   retroknowledge : Retroknowledge.retroknowledge;
   indirect_pterms : Opaqueproof.opaquetab;
-  native_symbols : Nativevalues.symbols DPmap.t;
 }
 
 let empty_named_context_val = {
@@ -136,7 +134,6 @@ let empty_env = {
   env_typing_flags = Declareops.safe_flags Conv_oracle.empty;
   retroknowledge = Retroknowledge.empty;
   indirect_pterms = Opaqueproof.empty_opaquetab;
-  native_symbols = DPmap.empty;
 }
 
 
@@ -482,6 +479,9 @@ let set_typing_flags c env =
     let env = set_type_in_type (not c.check_universes) env in
     env
 
+let update_typing_flags ?typing_flags env =
+  Option.cata (fun flags -> set_typing_flags flags env) env typing_flags
+
 let set_cumulative_sprop b env =
   set_typing_flags {env.env_typing_flags with cumulative_sprop=b} env
 
@@ -571,6 +571,11 @@ let is_primitive env c =
   | Declarations.Primitive _ -> true
   | _ -> false
 
+let is_array_type env c =
+  match env.retroknowledge.Retroknowledge.retro_array with
+  | None -> false
+  | Some c' -> Constant.CanOrd.equal c c'
+
 let polymorphic_constant cst env =
   Declareops.constant_is_polymorphic (lookup_constant cst env)
 
@@ -829,6 +834,65 @@ let is_type_in_type env r =
 
 let set_retroknowledge env r = { env with retroknowledge = r }
 
-let set_native_symbols env native_symbols = { env with native_symbols }
-let add_native_symbols dir syms env =
-  { env with native_symbols = DPmap.add dir syms env.native_symbols }
+module type QNameS =
+sig
+  type t
+  val equal : env -> t -> t -> bool
+  val compare : env -> t -> t -> int
+  val hash : env -> t -> int
+end
+
+module QConstant =
+struct
+  type t = Constant.t
+  let equal _env c1 c2 = Constant.CanOrd.equal c1 c2
+  let compare _env c1 c2 = Constant.CanOrd.compare c1 c2
+  let hash _env c = Constant.CanOrd.hash c
+end
+
+module QMutInd =
+struct
+  type t = MutInd.t
+  let equal _env c1 c2 = MutInd.CanOrd.equal c1 c2
+  let compare _env c1 c2 = MutInd.CanOrd.compare c1 c2
+  let hash _env c = MutInd.CanOrd.hash c
+end
+
+module QInd =
+struct
+  type t = Ind.t
+  let equal _env c1 c2 = Ind.CanOrd.equal c1 c2
+  let compare _env c1 c2 = Ind.CanOrd.compare c1 c2
+  let hash _env c = Ind.CanOrd.hash c
+end
+
+module QConstruct =
+struct
+  type t = Construct.t
+  let equal _env c1 c2 = Construct.CanOrd.equal c1 c2
+  let compare _env c1 c2 = Construct.CanOrd.compare c1 c2
+  let hash _env c = Construct.CanOrd.hash c
+end
+
+module QProjection =
+struct
+  type t = Projection.t
+  let equal _env c1 c2 = Projection.CanOrd.equal c1 c2
+  let compare _env c1 c2 = Projection.CanOrd.compare c1 c2
+  let hash _env c = Projection.CanOrd.hash c
+  module Repr =
+  struct
+    type t = Projection.Repr.t
+    let equal _env c1 c2 = Projection.Repr.CanOrd.equal c1 c2
+    let compare _env c1 c2 = Projection.Repr.CanOrd.compare c1 c2
+    let hash _env c = Projection.Repr.CanOrd.hash c
+  end
+end
+
+module QGlobRef =
+struct
+  type t = GlobRef.t
+  let equal _env c1 c2 = GlobRef.CanOrd.equal c1 c2
+  let compare _env c1 c2 = GlobRef.CanOrd.compare c1 c2
+  let hash _env c = GlobRef.CanOrd.hash c
+end