Merge PR #9909: Remove all but one call to `Global` in the pretyper

Ack-by: ejgallego
Reviewed-by: gares
Ack-by: maximedenes
Ack-by: ppedrot

22 files changed, 302 insertions, 635 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e22368d5e5..d7a6c4c832 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -284,7 +284,7 @@ let rec find_row_ind = function
 
 let inductive_template env sigma tmloc ind =
   let sigma, indu = Evd.fresh_inductive_instance env sigma ind in
-  let arsign = inductive_alldecls_env env indu in
+  let arsign = inductive_alldecls env indu in
   let indu = on_snd EInstance.make indu in
   let hole_source i = match tmloc with
     | Some loc -> Loc.tag ~loc @@ Evar_kinds.TomatchTypeParameter (ind,i)
@@ -313,7 +313,7 @@ let try_find_ind env sigma typ realnames =
       | Some names -> names
       | None ->
           let ind = fst (fst (dest_ind_family indf)) in
-          List.make (inductive_nrealdecls ind) Anonymous in
+          List.make (inductive_nrealdecls env ind) Anonymous in
   IsInd (typ,ind,names)
 
 let inh_coerce_to_ind env sigma0 loc ty tyi =
@@ -1796,7 +1796,7 @@ let build_inversion_problem ~program_mode loc env sigma tms t =
     | Construct (cstr,u) -> DAst.make (PatCstr (cstr,[],Anonymous)), acc
     | App (f,v) when isConstruct sigma f ->
 	let cstr,u = destConstruct sigma f in
-        let n = constructor_nrealargs_env !!env cstr in
+        let n = constructor_nrealargs !!env cstr in
 	let l = List.lastn n (Array.to_list v) in
 	let l,acc = List.fold_right_map reveal_pattern l acc in
 	DAst.make (PatCstr (cstr,l,Anonymous)), acc
@@ -1929,7 +1929,7 @@ let extract_arity_signature ?(dolift=true) env0 tomatchl tmsign =
       | IsInd (term,IndType(indf,realargs),_) ->
           let indf' = if dolift then lift_inductive_family n indf else indf in
 	  let ((ind,u),_) = dest_ind_family indf' in
-	  let nrealargs_ctxt = inductive_nrealdecls_env env0 ind in
+          let nrealargs_ctxt = inductive_nrealdecls env0 ind in
           let arsign, inds = get_arity env0 indf' in
 	  let arsign = List.map (fun d -> map_rel_decl EConstr.of_constr d) arsign in
           let realnal =
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 5560e5e5f5..90ce1cc594 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -15,7 +15,6 @@ open Names
 open Constr
 open Libnames
 open Globnames
-open Libobject
 open Mod_subst
 
 (* usage qque peu general: utilise aussi dans record *)
@@ -288,7 +287,7 @@ let get_coercion_constructor env coe =
   let red x = fst (Reductionops.whd_all_stack env evd x) in
   match EConstr.kind evd (red (mkNamed coe.coe_value)) with
   | Constr.Construct (c, _) ->
-      c, Inductiveops.constructor_nrealargs c -1
+      c, Inductiveops.constructor_nrealargs env c -1
   | _ -> raise Not_found
 
 let lookup_pattern_path_between env (s,t) =
@@ -305,8 +304,8 @@ let install_path_printer f = path_printer := f
 
 let print_path x = !path_printer x
 
-let path_comparator : (inheritance_path -> inheritance_path -> bool) ref =
-  ref (fun _ _ -> false)
+let path_comparator : (Environ.env -> Evd.evar_map -> inheritance_path -> inheritance_path -> bool) ref =
+  ref (fun _ _ _ _ -> false)
 
 let install_path_comparator f = path_comparator := f
 
@@ -319,24 +318,24 @@ let warn_ambiguous_path =
 (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
                          coercion,source,target *)
 
-let different_class_params i =
+let different_class_params env i =
   let ci = class_info_from_index i in
     if (snd ci).cl_param > 0 then true
     else 
       match fst ci with
-      | CL_IND i -> Global.is_polymorphic (IndRef i)
-      | CL_CONST c -> Global.is_polymorphic (ConstRef c)
+      | CL_IND i -> Environ.is_polymorphic env (IndRef i)
+      | CL_CONST c -> Environ.is_polymorphic env (ConstRef c)
       | _ -> false
 
-let add_coercion_in_graph (ic,source,target) =
+let add_coercion_in_graph env sigma (ic,source,target) =
   let old_inheritance_graph = !inheritance_graph in
   let ambig_paths =
     (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
   let try_add_new_path (i,j as ij) p =
-    if not (Bijint.Index.equal i j) || different_class_params i then
+    if not (Bijint.Index.equal i j) || different_class_params env i then
       match lookup_path_between_class ij with
       | q ->
-        if not (compare_path p q) then
+        if not (compare_path env sigma p q) then
           ambig_paths := (ij,p)::!ambig_paths;
         false
       | exception Not_found -> (add_new_path ij p; true)
@@ -374,31 +373,42 @@ type coercion = {
   coercion_params : int;
 }
 
+let subst_coercion subst c =
+  let coe = subst_coe_typ subst c.coercion_type in
+  let cls = subst_cl_typ subst c.coercion_source in
+  let clt = subst_cl_typ subst c.coercion_target in
+  let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in
+  if c.coercion_type == coe && c.coercion_source == cls &&
+     c.coercion_target == clt && c.coercion_is_proj == clp
+  then c
+  else { c with coercion_type = coe; coercion_source = cls;
+                coercion_target = clt; coercion_is_proj = clp; }
+
 (* Computation of the class arity *)
 
-let reference_arity_length ref =
-  let t, _ = Typeops.type_of_global_in_context (Global.env ()) ref in
-  List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *)
+let reference_arity_length env sigma ref =
+  let t, _ = Typeops.type_of_global_in_context env ref in
+  List.length (fst (Reductionops.splay_arity env sigma (EConstr.of_constr t)))
 
-let projection_arity_length p =
-  let len = reference_arity_length (ConstRef (Projection.Repr.constant p)) in
+let projection_arity_length env sigma p =
+  let len = reference_arity_length env sigma (ConstRef (Projection.Repr.constant p)) in
   len - Projection.Repr.npars p
 
-let class_params = function
+let class_params env sigma = function
   | CL_FUN | CL_SORT -> 0
-  | CL_CONST sp -> reference_arity_length (ConstRef sp)
-  | CL_PROJ sp -> projection_arity_length sp
-  | CL_SECVAR sp -> reference_arity_length (VarRef sp)
-  | CL_IND sp  -> reference_arity_length (IndRef sp)
+  | CL_CONST sp -> reference_arity_length env sigma (ConstRef sp)
+  | CL_PROJ sp -> projection_arity_length env sigma sp
+  | CL_SECVAR sp -> reference_arity_length env sigma (VarRef sp)
+  | CL_IND sp  -> reference_arity_length env sigma (IndRef sp)
 
 (* add_class : cl_typ -> locality_flag option -> bool -> unit *)
 
-let add_class cl =
-  add_new_class cl { cl_param = class_params cl }
+let add_class env sigma cl =
+  add_new_class cl { cl_param = class_params env sigma cl }
 
-let cache_coercion (_, c) =
-  let () = add_class c.coercion_source in
-  let () = add_class c.coercion_target in
+let declare_coercion env sigma c =
+  let () = add_class env sigma c.coercion_source in
+  let () = add_class env sigma c.coercion_target in
   let is, _ = class_info c.coercion_source in
   let it, _ = class_info c.coercion_target in
   let xf =
@@ -409,65 +419,7 @@ let cache_coercion (_, c) =
       coe_param = c.coercion_params;
     } in
   let () = add_new_coercion c.coercion_type xf in
-  add_coercion_in_graph (xf,is,it)
-
-let open_coercion i o =
-  if Int.equal i 1 then
-    cache_coercion o
-
-let subst_coercion (subst, c) =
-  let coe = subst_coe_typ subst c.coercion_type in
-  let cls = subst_cl_typ subst c.coercion_source in
-  let clt = subst_cl_typ subst c.coercion_target in
-  let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in
-  if c.coercion_type == coe && c.coercion_source == cls &&
-     c.coercion_target == clt && c.coercion_is_proj == clp
-  then c
-  else { c with coercion_type = coe; coercion_source = cls;
-                coercion_target = clt; coercion_is_proj = clp; }
-
-let discharge_coercion (_, c) =
-  if c.coercion_local then None
-  else
-    let n =
-      try
-        let ins = Lib.section_instance c.coercion_type in
-        Array.length (snd ins)
-      with Not_found -> 0
-    in
-    let nc = { c with
-      coercion_params = n + c.coercion_params;
-      coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj;
-    } in
-    Some nc
-
-let classify_coercion obj =
-  if obj.coercion_local then Dispose else Substitute obj
-
-let inCoercion : coercion -> obj =
-  declare_object {(default_object "COERCION") with
-    open_function = open_coercion;
-    cache_function = cache_coercion;
-    subst_function = subst_coercion;
-    classify_function = classify_coercion;
-    discharge_function = discharge_coercion }
-
-let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps =
-  let isproj = 
-    match coef with
-    | ConstRef c -> Recordops.find_primitive_projection c
-    | _ -> None
-  in
-  let c = {
-    coercion_type = coef;
-    coercion_local = local;
-    coercion_is_id = isid;
-    coercion_is_proj = isproj;
-    coercion_source = cls;
-    coercion_target = clt;
-    coercion_params = ps;
-  } in
-  Lib.add_anonymous_leaf (inCoercion c)
+  add_coercion_in_graph env sigma (xf,is,it)
 
 (* For printing purpose *)
 let pr_cl_index = Bijint.Index.print
@@ -490,7 +442,7 @@ module CoercionPrinting =
   struct
     type t = coe_typ
     let compare = GlobRef.Ordered.compare
-    let encode = coercion_of_reference
+    let encode _env = coercion_of_reference
     let subst = subst_coe_typ
     let printer x = Nametab.pr_global_env Id.Set.empty x
     let key = ["Printing";"Coercion"]
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index bd468e62ad..c04182930e 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -75,9 +75,19 @@ val inductive_class_of : inductive -> cl_index
 val class_args_of : env -> evar_map -> types -> constr list
 
 (** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *)
-val declare_coercion :
-  coe_typ -> ?local:bool -> isid:bool ->
-      src:cl_typ -> target:cl_typ -> params:int -> unit
+type coercion = {
+  coercion_type   : coe_typ;
+  coercion_local  : bool;
+  coercion_is_id  : bool;
+  coercion_is_proj  : Projection.Repr.t option;
+  coercion_source : cl_typ;
+  coercion_target : cl_typ;
+  coercion_params : int;
+}
+
+val subst_coercion : substitution -> coercion -> coercion
+
+val declare_coercion : env -> evar_map -> coercion -> unit
 
 (** {6 Access to coercions infos } *)
 val coercion_exists : coe_typ -> bool
@@ -101,7 +111,7 @@ val lookup_pattern_path_between :
 val install_path_printer :
   ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
 val install_path_comparator :
-  (inheritance_path -> inheritance_path -> bool) -> unit
+  (env -> evar_map -> inheritance_path -> inheritance_path -> bool) -> unit
 (**/**)
 
 (** {6 This is for printing purpose } *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 87d3880f99..eaa5736336 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -145,9 +145,9 @@ let add_name_opt na b t (nenv, env) =
 (****************************************************************************)
 (* Tools for printing of Cases                                              *)
 
-let encode_inductive r =
+let encode_inductive env r =
   let indsp = Nametab.global_inductive r in
-  let constr_lengths = constructors_nrealargs indsp in
+  let constr_lengths = constructors_nrealargs env indsp in
   (indsp,constr_lengths)
 
 (* Parameterization of the translation from constr to ast      *)
@@ -159,15 +159,15 @@ let has_two_constructors lc =
 
 let isomorphic_to_tuple lc = Int.equal (Array.length lc) 1
 
-let encode_bool ({CAst.loc} as r) =
-  let (x,lc) = encode_inductive r in
+let encode_bool env ({CAst.loc} as r) =
+  let (x,lc) = encode_inductive env r in
   if not (has_two_constructors lc) then
     user_err ?loc ~hdr:"encode_if"
       (str "This type has not exactly two constructors.");
   x
 
-let encode_tuple ({CAst.loc} as r) =
-  let (x,lc) = encode_inductive r in
+let encode_tuple env ({CAst.loc} as r) =
+  let (x,lc) = encode_inductive env r in
   if not (isomorphic_to_tuple lc) then
     user_err ?loc ~hdr:"encode_tuple"
       (str "This type cannot be seen as a tuple type.");
@@ -175,7 +175,7 @@ let encode_tuple ({CAst.loc} as r) =
 
 module PrintingInductiveMake =
   functor (Test : sig
-     val encode : qualid -> inductive
+     val encode : Environ.env -> qualid -> inductive
      val member_message : Pp.t -> bool -> Pp.t
      val field : string
      val title : string
@@ -1014,13 +1014,12 @@ let rec subst_cases_pattern subst = DAst.map (function
 
 let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
 
-let rec subst_glob_constr subst = DAst.map (function
+let rec subst_glob_constr env subst = DAst.map (function
   | GRef (ref,u) as raw ->
     let ref',t = subst_global subst ref in
     if ref' == ref then raw else (match t with
         | None -> GRef (ref', u)
         | Some t ->
-          let env = Global.env () in
           let evd = Evd.from_env env in
           let t = t.Univ.univ_abstracted_value in (* XXX This seems dangerous *)
           DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t)))
@@ -1032,33 +1031,33 @@ let rec subst_glob_constr subst = DAst.map (function
   | GPatVar _ as raw -> raw
 
   | GApp (r,rl) as raw ->
-      let r' = subst_glob_constr subst r
-      and rl' = List.Smart.map (subst_glob_constr subst) rl in
+      let r' = subst_glob_constr env subst r
+      and rl' = List.Smart.map (subst_glob_constr env subst) rl in
 	if r' == r && rl' == rl then raw else
 	  GApp(r',rl')
 
   | GLambda (n,bk,r1,r2) as raw ->
-      let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
+      let r1' = subst_glob_constr env subst r1 and r2' = subst_glob_constr env subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
 	  GLambda (n,bk,r1',r2')
 
   | GProd (n,bk,r1,r2) as raw ->
-      let r1' = subst_glob_constr subst r1 and r2' = subst_glob_constr subst r2 in
+      let r1' = subst_glob_constr env subst r1 and r2' = subst_glob_constr env subst r2 in
 	if r1' == r1 && r2' == r2 then raw else
 	  GProd (n,bk,r1',r2')
 
   | GLetIn (n,r1,t,r2) as raw ->
-      let r1' = subst_glob_constr subst r1 in
-      let r2' = subst_glob_constr subst r2 in
-      let t' = Option.Smart.map (subst_glob_constr subst) t in
+      let r1' = subst_glob_constr env subst r1 in
+      let r2' = subst_glob_constr env subst r2 in
+      let t' = Option.Smart.map (subst_glob_constr env subst) t in
 	if r1' == r1 && t == t' && r2' == r2 then raw else
 	  GLetIn (n,r1',t',r2')
 
   | GCases (sty,rtno,rl,branches) as raw ->
     let open CAst in
-      let rtno' = Option.Smart.map (subst_glob_constr subst) rtno
+      let rtno' = Option.Smart.map (subst_glob_constr env subst) rtno
       and rl' = List.Smart.map (fun (a,x as y) ->
-        let a' = subst_glob_constr subst a in
+        let a' = subst_glob_constr env subst a in
         let (n,topt) = x in
         let topt' = Option.Smart.map
           (fun ({loc;v=((sp,i),y)} as t) ->
@@ -1069,7 +1068,7 @@ let rec subst_glob_constr subst = DAst.map (function
                         (fun ({loc;v=(idl,cpl,r)} as branch) ->
 			   let cpl' =
                              List.Smart.map (subst_cases_pattern subst) cpl
-			   and r' = subst_glob_constr subst r in
+                           and r' = subst_glob_constr env subst r in
 			     if cpl' == cpl && r' == r then branch else
                                CAst.(make ?loc (idl,cpl',r')))
 			branches
@@ -1078,27 +1077,27 @@ let rec subst_glob_constr subst = DAst.map (function
 	  GCases (sty,rtno',rl',branches')
 
   | GLetTuple (nal,(na,po),b,c) as raw ->
-      let po' = Option.Smart.map (subst_glob_constr subst) po
-      and b' = subst_glob_constr subst b
-      and c' = subst_glob_constr subst c in
+      let po' = Option.Smart.map (subst_glob_constr env subst) po
+      and b' = subst_glob_constr env subst b
+      and c' = subst_glob_constr env subst c in
 	if po' == po && b' == b && c' == c then raw else
           GLetTuple (nal,(na,po'),b',c')
 
   | GIf (c,(na,po),b1,b2) as raw ->
-      let po' = Option.Smart.map (subst_glob_constr subst) po
-      and b1' = subst_glob_constr subst b1
-      and b2' = subst_glob_constr subst b2
-      and c' = subst_glob_constr subst c in
+      let po' = Option.Smart.map (subst_glob_constr env subst) po
+      and b1' = subst_glob_constr env subst b1
+      and b2' = subst_glob_constr env subst b2
+      and c' = subst_glob_constr env subst c in
 	if c' == c && po' == po && b1' == b1 && b2' == b2 then raw else
           GIf (c',(na,po'),b1',b2')
 
   | GRec (fix,ida,bl,ra1,ra2) as raw ->
-      let ra1' = Array.Smart.map (subst_glob_constr subst) ra1
-      and ra2' = Array.Smart.map (subst_glob_constr subst) ra2 in
+      let ra1' = Array.Smart.map (subst_glob_constr env subst) ra1
+      and ra2' = Array.Smart.map (subst_glob_constr env subst) ra2 in
       let bl' = Array.Smart.map
         (List.Smart.map (fun (na,k,obd,ty as dcl) ->
-          let ty' = subst_glob_constr subst ty in
-          let obd' = Option.Smart.map (subst_glob_constr subst) obd in
+          let ty' = subst_glob_constr env subst ty in
+          let obd' = Option.Smart.map (subst_glob_constr env subst) obd in
           if ty'==ty && obd'==obd then dcl else (na,k,obd',ty')))
         bl in
 	if ra1' == ra1 && ra2' == ra2 && bl'==bl then raw else
@@ -1116,8 +1115,8 @@ let rec subst_glob_constr subst = DAst.map (function
     else GHole (nknd, naming, nsolve)
 
   | GCast (r1,k) as raw ->
-      let r1' = subst_glob_constr subst r1 in
-      let k' = smartmap_cast_type (subst_glob_constr subst) k in
+      let r1' = subst_glob_constr env subst r1 in
+      let k' = smartmap_cast_type (subst_glob_constr env subst) k in
       if r1' == r1 && k' == k then raw else GCast (r1',k')
 
   )
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 8695d52b12..1a8e97efb8 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -37,7 +37,7 @@ val print_allow_match_default_clause : bool ref
 
 val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern
 
-val subst_glob_constr : substitution -> glob_constr -> glob_constr
+val subst_glob_constr : env -> substitution -> glob_constr -> glob_constr
 
 val factorize_eqns : 'a cases_clauses_g -> 'a disjunctive_cases_clauses_g
 
@@ -87,7 +87,7 @@ val subst_genarg_hook :
 
 module PrintingInductiveMake :
   functor (Test : sig
-    val encode : Libnames.qualid -> Names.inductive
+    val encode : Environ.env -> Libnames.qualid -> Names.inductive
     val member_message : Pp.t -> bool -> Pp.t
     val field : string
     val title : string
@@ -95,7 +95,7 @@ module PrintingInductiveMake :
     sig
       type t = Names.inductive
       val compare : t -> t -> int
-      val encode : Libnames.qualid -> Names.inductive
+      val encode : Environ.env -> Libnames.qualid -> Names.inductive
       val subst : substitution -> t -> t
       val printer : t -> Pp.t
       val key : Goptions.option_name
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index a4a078bfa0..4a941a68b1 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -73,11 +73,11 @@ let normalize_evar evd ev =
   | Evar (evk,args) -> (evk,args)
   | _ -> assert false
 
-let get_polymorphic_positions sigma f =
+let get_polymorphic_positions env sigma f =
   let open Declarations in
   match EConstr.kind sigma f with
-  | Ind (ind, u) | Construct ((ind, _), u) -> 
-    let mib,oib = Global.lookup_inductive ind in
+  | Ind (ind, u) | Construct ((ind, _), u) ->
+    let mib,oib = Inductive.lookup_mind_specif env ind in
       (match oib.mind_arity with
       | RegularArity _ -> assert false
       | TemplateArity templ -> templ.template_param_levels)
@@ -128,7 +128,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
   let rec refresh_term_evars ~onevars ~top t =
     match EConstr.kind !evdref t with
     | App (f, args) when Termops.is_template_polymorphic_ind env !evdref f ->
-      let pos = get_polymorphic_positions !evdref f in
+      let pos = get_polymorphic_positions env !evdref f in
         refresh_polymorphic_positions args pos; t
     | App (f, args) when top && isEvar !evdref f -> 
        let f' = refresh_term_evars ~onevars:true ~top:false f in
@@ -1203,17 +1203,17 @@ exception CannotProject of evar_map * EConstr.existential
   of subterms to eventually discard so as to be allowed to keep ti.
 *)
 
-let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t =
+let rec is_constrainable_in top env evd k (ev,(fv_rels,fv_ids) as g) t =
   let f,args = decompose_app_vect evd t in
   match EConstr.kind evd f with
   | Construct ((ind,_),u) ->
-    let n = Inductiveops.inductive_nparams ind in
+    let n = Inductiveops.inductive_nparams env ind in
     if n > Array.length args then true (* We don't try to be more clever *)
     else
       let params = fst (Array.chop n args) in
-      Array.for_all (is_constrainable_in false evd k g) params
-  | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args
-  | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2
+      Array.for_all (is_constrainable_in false env evd k g) params
+  | Ind _ -> Array.for_all (is_constrainable_in false env evd k g) args
+  | Prod (na,t1,t2) -> is_constrainable_in false env evd k g t1 && is_constrainable_in false env evd k g t2
   | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*)
   | Var id -> Id.Set.mem id fv_ids
   | Rel n -> n <= k || Int.Set.mem n fv_rels
@@ -1238,7 +1238,7 @@ let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_r
   | None ->
     (* t is an instance for a proper variable; we filter it along *)
     (* the free variables allowed to occur *)
-    (not force || noccur_evar env evd ev t) && is_constrainable_in true evd k (ev,(fv_rels,fv_ids)) t
+    (not force || noccur_evar env evd ev t) && is_constrainable_in true env evd k (ev,(fv_rels,fv_ids)) t
 
 exception EvarSolvedOnTheFly of evar_map * EConstr.constr
 
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 74432cc010..6da168711c 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -492,7 +492,7 @@ let is_gvar id c = match DAst.get c with
 | GVar id' -> Id.equal id id'
 | _ -> false
 
-let rec cases_pattern_of_glob_constr na c =
+let rec cases_pattern_of_glob_constr env na c =
   (* Forcing evaluation to ensure that the possible raising of
      Not_found is not delayed *)
   let c = DAst.force c in
@@ -509,14 +509,14 @@ let rec cases_pattern_of_glob_constr na c =
   | GApp (c, l) ->
     begin match DAst.get c with
     | GRef (ConstructRef cstr,_) ->
-      let nparams = Inductiveops.inductive_nparams (fst cstr) in
+      let nparams = Inductiveops.inductive_nparams env (fst cstr) in
       let _,l = List.chop nparams l in
-      PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
+      PatCstr (cstr,List.map (cases_pattern_of_glob_constr env Anonymous) l,na)
     | _ -> raise Not_found
     end
   | GLetIn (Name id as na',b,None,e) when is_gvar id e && na = Anonymous ->
      (* A canonical encoding of aliases *)
-     DAst.get (cases_pattern_of_glob_constr na' b)
+     DAst.get (cases_pattern_of_glob_constr env na' b)
   | _ -> raise Not_found
   ) c
 
@@ -539,8 +539,8 @@ let drop_local_defs params decls args =
       | _ -> assert false in
     aux decls args
 
-let add_patterns_for_params_remove_local_defs (ind,j) l =
-  let (mib,mip) = Global.lookup_inductive ind in
+let add_patterns_for_params_remove_local_defs env (ind,j) l =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let nparams = mib.Declarations.mind_nparams in
   let l =
     if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then
@@ -556,12 +556,12 @@ let add_alias ?loc na c =
   | Name id -> GLetIn (na,DAst.make ?loc c,None,DAst.make ?loc (GVar id))
 
 (* Turn a closed cases pattern into a glob_constr *)
-let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?loc -> function
+let rec glob_constr_of_cases_pattern_aux env isclosed x = DAst.map_with_loc (fun ?loc -> function
   | PatCstr (cstr,[],na) -> add_alias ?loc na (GRef (ConstructRef cstr,None))
   | PatCstr (cstr,l,na)  ->
       let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in
-      let l = add_patterns_for_params_remove_local_defs cstr l in
-      add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux isclosed) l))
+      let l = add_patterns_for_params_remove_local_defs env cstr l in
+      add_alias ?loc na (GApp (ref, List.map (glob_constr_of_cases_pattern_aux env isclosed) l))
   | PatVar (Name id) when not isclosed ->
       GVar id
   | PatVar Anonymous when not isclosed ->
@@ -571,14 +571,14 @@ let rec glob_constr_of_cases_pattern_aux isclosed x = DAst.map_with_loc (fun ?lo
   | _ -> raise Not_found
   ) x
 
-let glob_constr_of_closed_cases_pattern p = match DAst.get p with
+let glob_constr_of_closed_cases_pattern env p = match DAst.get p with
   | PatCstr (cstr,l,na) ->
       let loc = p.CAst.loc in
-      na,glob_constr_of_cases_pattern_aux true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
+      na,glob_constr_of_cases_pattern_aux env true (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
   | _ ->
       raise Not_found
 
-let glob_constr_of_cases_pattern p = glob_constr_of_cases_pattern_aux false p
+let glob_constr_of_cases_pattern env p = glob_constr_of_cases_pattern_aux env false p
 
 (* This has to be in some file... *)
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 2f0ac76235..df902a8fa7 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -94,14 +94,15 @@ val map_pattern : (glob_constr -> glob_constr) ->
     Evaluation is forced.
     Take the current alias as parameter,
     @raise Not_found if translation is impossible *)
-val cases_pattern_of_glob_constr : Name.t -> 'a glob_constr_g -> 'a cases_pattern_g
+val cases_pattern_of_glob_constr : Environ.env -> Name.t -> 'a glob_constr_g -> 'a cases_pattern_g
 
-val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob_constr_g
+val glob_constr_of_closed_cases_pattern : Environ.env -> 'a cases_pattern_g -> Name.t * 'a glob_constr_g
 
 (** A canonical encoding of cases pattern into constr such that
     composed with [cases_pattern_of_glob_constr Anonymous] gives identity *)
-val glob_constr_of_cases_pattern : 'a cases_pattern_g -> 'a glob_constr_g
+val glob_constr_of_cases_pattern : Environ.env -> 'a cases_pattern_g -> 'a glob_constr_g
 
-val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list
+val add_patterns_for_params_remove_local_defs : Environ.env -> constructor ->
+  'a cases_pattern_g list -> 'a cases_pattern_g list
 
 val empty_lvar : Ltac_pretype.ltac_var_map
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index 7590ac301b..ef27ca9b4e 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -33,17 +33,16 @@ type head_approximation =
 | NotImmediatelyComputableHead
 
 (* FIXME: maybe change interface here *)
-let rec compute_head = function
+let rec compute_head env = function
   | EvalConstRef cst ->
-    let env = Global.env() in
     let body = Environ.constant_opt_value_in env (cst,Univ.Instance.empty) in
     (match body with
      | None -> RigidHead (RigidParameter cst)
      | Some c -> kind_of_head env c)
   | EvalVarRef id ->
-    (match Global.lookup_named id with
+    (match lookup_named id env with
      | LocalDef (_,c,_) when not (Decls.variable_opacity id) ->
-       kind_of_head (Global.env()) c
+       kind_of_head env c
      | _ -> RigidHead RigidOther)
 
 and kind_of_head env t =
@@ -51,14 +50,14 @@ and kind_of_head env t =
   | Rel n when n > k -> NotImmediatelyComputableHead
   | Rel n -> FlexibleHead (k,k+1-n,List.length l,b)
   | Var id ->
-      (try on_subterm k l b (compute_head (EvalVarRef id))
+      (try on_subterm k l b (compute_head env (EvalVarRef id))
        with Not_found ->
         (* a goal variable *)
         match lookup_named id env with
         | LocalDef (_,c,_) -> aux k l c b
         | LocalAssum _ -> NotImmediatelyComputableHead)
   | Const (cst,_) ->
-      (try on_subterm k l b (compute_head (EvalConstRef cst))
+      (try on_subterm k l b (compute_head env (EvalConstRef cst))
        with Not_found ->
          CErrors.anomaly
            Pp.(str "constant not found in kind_of_head: " ++
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 4f940fa16a..7615a17514 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -610,16 +610,20 @@ let make_elimination_ident id s = add_suffix id (elimination_suffix s)
 
 (* Look up function for the default elimination constant *)
 
-let lookup_eliminator ind_sp s =
+let lookup_eliminator env ind_sp s =
   let kn,i = ind_sp in
-  let mp,l = KerName.repr (MutInd.canonical kn) in
-  let ind_id = (Global.lookup_mind kn).mind_packets.(i).mind_typename in
+  let mpu = KerName.modpath @@ MutInd.user kn in
+  let mpc = KerName.modpath @@ MutInd.canonical kn in
+  let ind_id = (lookup_mind kn env).mind_packets.(i).mind_typename in
   let id = add_suffix ind_id (elimination_suffix s) in
+  let l = Label.of_id id in
+  let knu = KerName.make mpu l in
+  let knc = KerName.make mpc l in
   (* Try first to get an eliminator defined in the same section as the *)
   (* inductive type *)
   try
-    let cst =Global.constant_of_delta_kn (KerName.make mp (Label.of_id id)) in
-    let _ = Global.lookup_constant cst in
+    let cst = Constant.make knu knc in
+    let _ = lookup_constant cst env in
       ConstRef cst
   with Not_found ->
   (* Then try to get a user-defined eliminator in some other places *)
diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli
index 91a5651f7f..8eb571a8be 100644
--- a/pretyping/indrec.mli
+++ b/pretyping/indrec.mli
@@ -62,7 +62,7 @@ val weaken_sort_scheme : env -> evar_map -> bool -> Sorts.t -> int -> constr ->
 
 (** Recursor names utilities *)
 
-val lookup_eliminator : inductive -> Sorts.family -> GlobRef.t
+val lookup_eliminator : env -> inductive -> Sorts.family -> GlobRef.t
 val elimination_suffix : Sorts.family -> string
 val make_elimination_ident : Id.t -> Sorts.family -> Id.t
 
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 678aebfbe6..b1c98da2c7 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -112,162 +112,145 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j =
 
 (* Number of constructors *)
 
-let nconstructors ind =
-  let (_,mip) = Global.lookup_inductive ind in
-  Array.length mip.mind_consnames
-
-let nconstructors_env env ind =
+let nconstructors env ind =
   let (_,mip) = Inductive.lookup_mind_specif env ind in
   Array.length mip.mind_consnames
 
-(* Arity of constructors excluding parameters, excluding local defs *)
+let nconstructors_env env ind = nconstructors env ind
+[@@ocaml.deprecated "Alias for Inductiveops.nconstructors"]
 
-let constructors_nrealargs ind =
-  let (_,mip) = Global.lookup_inductive ind in
-  mip.mind_consnrealargs
+(* Arity of constructors excluding parameters, excluding local defs *)
 
-let constructors_nrealargs_env env ind =
+let constructors_nrealargs env ind =
   let (_,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_consnrealargs
 
-(* Arity of constructors excluding parameters, including local defs *)
+let constructors_nrealargs_env env ind = constructors_nrealargs env ind
+[@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealargs"]
 
-let constructors_nrealdecls ind =
-  let (_,mip) = Global.lookup_inductive ind in
-  mip.mind_consnrealdecls
+(* Arity of constructors excluding parameters, including local defs *)
 
-let constructors_nrealdecls_env env ind =
+let constructors_nrealdecls env ind =
   let (_,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_consnrealdecls
 
+let constructors_nrealdecls_env env ind = constructors_nrealdecls env ind
+[@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealdecls"]
+
 (* Arity of constructors including parameters, excluding local defs *)
 
-let constructor_nallargs (indsp,j) =
-  let (mib,mip) = Global.lookup_inductive indsp in
+let constructor_nallargs env (ind,j) =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_consnrealargs.(j-1) + mib.mind_nparams
 
-let constructor_nallargs_env env ((kn,i),j) =
-  let mib = Environ.lookup_mind kn env in
-  let mip = mib.mind_packets.(i) in
-  mip.mind_consnrealargs.(j-1) + mib.mind_nparams
+let constructor_nallargs_env env (indsp,j) = constructor_nallargs env (indsp,j)
+[@@ocaml.deprecated "Alias for Inductiveops.constructor_nallargs"]
 
 (* Arity of constructors including params, including local defs *)
 
-let constructor_nalldecls (indsp,j) = (* TOCHANGE en decls *)
-  let (mib,mip) = Global.lookup_inductive indsp in
+let constructor_nalldecls env (ind,j) = (* TOCHANGE en decls *)
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt)
 
-let constructor_nalldecls_env env ((kn,i),j) = (* TOCHANGE en decls *)
-  let mib = Environ.lookup_mind kn env in
-  let mip = mib.mind_packets.(i) in
-  mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt)
+let constructor_nalldecls_env env (indsp,j) = constructor_nalldecls env (indsp,j)
+[@@ocaml.deprecated "Alias for Inductiveops.constructor_nalldecls"]
 
 (* Arity of constructors excluding params, excluding local defs *)
 
-let constructor_nrealargs (ind,j) =
-  let (_,mip) = Global.lookup_inductive ind in
-  mip.mind_consnrealargs.(j-1)
-
-let constructor_nrealargs_env env (ind,j) =
+let constructor_nrealargs env (ind,j) =
   let (_,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_consnrealargs.(j-1)
 
-(* Arity of constructors excluding params, including local defs *)
+let constructor_nrealargs_env env (ind,j) = constructor_nrealargs env (ind,j)
+[@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealargs"]
 
-let constructor_nrealdecls (ind,j) = (* TOCHANGE en decls *)
-  let (_,mip) = Global.lookup_inductive ind in
-  mip.mind_consnrealdecls.(j-1)
+(* Arity of constructors excluding params, including local defs *)
 
-let constructor_nrealdecls_env env (ind,j) = (* TOCHANGE en decls *)
+let constructor_nrealdecls env (ind,j) = (* TOCHANGE en decls *)
   let (_,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_consnrealdecls.(j-1)
 
-(* Length of arity, excluding params, excluding local defs *)
+let constructor_nrealdecls_env env (ind,j) = constructor_nrealdecls env (ind,j)
+[@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"]
 
-let inductive_nrealargs ind =
-  let (_,mip) = Global.lookup_inductive ind in
-  mip.mind_nrealargs
+(* Length of arity, excluding params, excluding local defs *)
 
-let inductive_nrealargs_env env ind =
+let inductive_nrealargs env ind =
   let (_,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_nrealargs
 
-(* Length of arity, excluding params, including local defs *)
+let inductive_nrealargs_env env ind = inductive_nrealargs env ind
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealargs"]
 
-let inductive_nrealdecls ind =
-  let (_,mip) = Global.lookup_inductive ind in
-  mip.mind_nrealdecls
+(* Length of arity, excluding params, including local defs *)
 
-let inductive_nrealdecls_env env ind =
+let inductive_nrealdecls env ind =
   let (_,mip) = Inductive.lookup_mind_specif env ind in
   mip.mind_nrealdecls
 
-(* Full length of arity (w/o local defs) *)
+let inductive_nrealdecls_env env ind = inductive_nrealdecls env ind
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealdecls"]
 
-let inductive_nallargs ind =
-  let (mib,mip) = Global.lookup_inductive ind in
-  mib.mind_nparams + mip.mind_nrealargs
+(* Full length of arity (w/o local defs) *)
 
-let inductive_nallargs_env env ind =
+let inductive_nallargs env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mib.mind_nparams + mip.mind_nrealargs
 
-(* Length of arity (w/o local defs) *)
+let inductive_nallargs_env env ind = inductive_nallargs env ind
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_nallargs"]
 
-let inductive_nparams ind =
-  let (mib,mip) = Global.lookup_inductive ind in
-  mib.mind_nparams
+(* Length of arity (w/o local defs) *)
 
-let inductive_nparams_env env ind =
+let inductive_nparams env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   mib.mind_nparams
 
-(* Length of arity (with local defs) *)
+let inductive_nparams_env env ind = inductive_nparams env ind
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_nparams"]
 
-let inductive_nparamdecls ind =
-  let (mib,mip) = Global.lookup_inductive ind in
-  Context.Rel.length mib.mind_params_ctxt
+(* Length of arity (with local defs) *)
 
-let inductive_nparamdecls_env env ind =
+let inductive_nparamdecls env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   Context.Rel.length mib.mind_params_ctxt
 
-(* Full length of arity (with local defs) *)
+let inductive_nparamdecls_env env ind = inductive_nparamdecls env ind
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_nparamsdecls"]
 
-let inductive_nalldecls ind =
-  let (mib,mip) = Global.lookup_inductive ind in
-  Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls
+(* Full length of arity (with local defs) *)
 
-let inductive_nalldecls_env env ind =
+let inductive_nalldecls env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls
 
-(* Others *)
+let inductive_nalldecls_env env ind = inductive_nalldecls env ind
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_nalldecls"]
 
-let inductive_paramdecls (ind,u) =
-  let (mib,mip) = Global.lookup_inductive ind in
-    Inductive.inductive_paramdecls (mib,u)
+(* Others *)
 
-let inductive_paramdecls_env env (ind,u) =
+let inductive_paramdecls env (ind,u) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
     Inductive.inductive_paramdecls (mib,u)
 
-let inductive_alldecls (ind,u) =
-  let (mib,mip) = Global.lookup_inductive ind in
-    Vars.subst_instance_context u mip.mind_arity_ctxt
+let inductive_paramdecls_env env (ind,u) = inductive_paramdecls env (ind,u)
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_paramsdecls"]
 
-let inductive_alldecls_env env (ind,u) =
+let inductive_alldecls env (ind,u) =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
     Vars.subst_instance_context u mip.mind_arity_ctxt
 
-let constructor_has_local_defs (indsp,j) =
-  let (mib,mip) = Global.lookup_inductive indsp in
+let inductive_alldecls_env env (ind,u) = inductive_alldecls env (ind,u)
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"]
+
+let constructor_has_local_defs env (indsp,j) =
+  let (mib,mip) = Inductive.lookup_mind_specif env indsp in
   let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in
   let l2 = recarg_length mip.mind_recargs j + mib.mind_nparams in
   not (Int.equal l1 l2)
 
-let inductive_has_local_defs ind =
-  let (mib,mip) = Global.lookup_inductive ind in
+let inductive_has_local_defs env ind =
+  let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let l1 = Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls in
   let l2 = mib.mind_nparams + mip.mind_nrealargs in
   not (Int.equal l1 l2)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index c74bbfe98b..cfc650938e 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -61,70 +61,85 @@ val mis_nf_constructor_type :
 (** {6 Extract information from an inductive name} *)
 
 (** @return number of constructors *)
-val nconstructors : inductive -> int
+val nconstructors : env -> inductive -> int
 val nconstructors_env : env -> inductive -> int
+[@@ocaml.deprecated "Alias for Inductiveops.nconstructors"]
 
 (** @return arity of constructors excluding parameters, excluding local defs *)
-val constructors_nrealargs : inductive -> int array
+val constructors_nrealargs : env -> inductive -> int array
 val constructors_nrealargs_env : env -> inductive -> int array
+[@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealargs"]
 
 (** @return arity of constructors excluding parameters, including local defs *)
-val constructors_nrealdecls : inductive -> int array
+val constructors_nrealdecls : env -> inductive -> int array
 val constructors_nrealdecls_env : env -> inductive -> int array
+[@@ocaml.deprecated "Alias for Inductiveops.constructors_nrealdecls"]
 
 (** @return the arity, excluding params, excluding local defs *)
-val inductive_nrealargs : inductive -> int
+val inductive_nrealargs : env -> inductive -> int
 val inductive_nrealargs_env : env -> inductive -> int
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealargs"]
 
 (** @return the arity, excluding params, including local defs *)
-val inductive_nrealdecls : inductive -> int
+val inductive_nrealdecls : env -> inductive -> int
 val inductive_nrealdecls_env : env -> inductive -> int
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_nrealdecls"]
 
 (** @return the arity, including params, excluding local defs *)
-val inductive_nallargs : inductive -> int
+val inductive_nallargs : env -> inductive -> int
 val inductive_nallargs_env : env -> inductive -> int
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_nallargs"]
 
 (** @return the arity, including params, including local defs *)
-val inductive_nalldecls : inductive -> int
+val inductive_nalldecls : env -> inductive -> int
 val inductive_nalldecls_env : env -> inductive -> int
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_nalldecls"]
 
 (** @return nb of params without local defs *)
-val inductive_nparams : inductive -> int
+val inductive_nparams : env -> inductive -> int
 val inductive_nparams_env : env -> inductive -> int
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_nparams"]
 
 (** @return nb of params with local defs *)
-val inductive_nparamdecls : inductive -> int
+val inductive_nparamdecls : env -> inductive -> int
 val inductive_nparamdecls_env : env -> inductive -> int
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_nparamsdecls"]
 
 (** @return params context *)
-val inductive_paramdecls : pinductive -> Constr.rel_context
+val inductive_paramdecls : env -> pinductive -> Constr.rel_context
 val inductive_paramdecls_env : env -> pinductive -> Constr.rel_context
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_paramsdecl"]
 
 (** @return full arity context, hence with letin *)
-val inductive_alldecls : pinductive -> Constr.rel_context
+val inductive_alldecls : env -> pinductive -> Constr.rel_context
 val inductive_alldecls_env : env -> pinductive -> Constr.rel_context
+[@@ocaml.deprecated "Alias for Inductiveops.inductive_alldecls"]
 
 (** {7 Extract information from a constructor name} *)
 
 (** @return param + args without letin *)
-val constructor_nallargs : constructor -> int
+val constructor_nallargs : env -> constructor -> int
 val constructor_nallargs_env : env -> constructor -> int
+[@@ocaml.deprecated "Alias for Inductiveops.constructor_nallargs"]
 
 (** @return param + args with letin *)
-val constructor_nalldecls : constructor -> int
+val constructor_nalldecls : env -> constructor -> int
 val constructor_nalldecls_env : env -> constructor -> int
+[@@ocaml.deprecated "Alias for Inductiveops.constructor_nalldecls"]
 
 (** @return args without letin *)
-val constructor_nrealargs : constructor -> int
+val constructor_nrealargs : env -> constructor -> int
 val constructor_nrealargs_env : env -> constructor -> int
+[@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealargs"]
 
 (** @return args with letin *)
-val constructor_nrealdecls : constructor -> int
+val constructor_nrealdecls : env -> constructor -> int
 val constructor_nrealdecls_env : env -> constructor -> int
+[@@ocaml.deprecated "Alias for Inductiveops.constructor_nrealdecls"]
 
 (** Is there local defs in params or args ? *)
-val constructor_has_local_defs : constructor -> bool
-val inductive_has_local_defs : inductive -> bool
+val constructor_has_local_defs : env -> constructor -> bool
+val inductive_has_local_defs : env -> inductive -> bool
 
 val allowed_sorts : env -> inductive -> Sorts.family list
 
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 4e3c77cb1a..b29afd1fd2 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -280,66 +280,64 @@ let rec liftn_pattern k n = function
 
 let lift_pattern k = liftn_pattern k 1
 
-let rec subst_pattern subst pat =
+let rec subst_pattern env sigma subst pat =
   match pat with
   | PRef ref ->
     let ref',t = subst_global subst ref in
     if ref' == ref then pat else (match t with
         | None -> PRef ref'
         | Some t ->
-          let env = Global.env () in
-          let evd = Evd.from_env env in
-          pattern_of_constr env evd t.Univ.univ_abstracted_value)
+          pattern_of_constr env sigma t.Univ.univ_abstracted_value)
   | PVar _
   | PEvar _
   | PRel _
   | PInt _ -> pat
   | PProj (p,c) -> 
       let p' = Projection.map (subst_mind subst) p in
-      let c' = subst_pattern subst c in
+      let c' = subst_pattern env sigma subst c in
 	if p' == p && c' == c then pat else
 	  PProj(p',c')
   | PApp (f,args) ->
-      let f' = subst_pattern subst f in
-      let args' = Array.Smart.map (subst_pattern subst) args in
+      let f' = subst_pattern env sigma subst f in
+      let args' = Array.Smart.map (subst_pattern env sigma subst) args in
 	if f' == f && args' == args then pat else
 	  PApp (f',args')
   | PSoApp (i,args) ->
-      let args' = List.Smart.map (subst_pattern subst) args in
+      let args' = List.Smart.map (subst_pattern env sigma subst) args in
 	if args' == args then pat else
 	  PSoApp (i,args')
   | PLambda (name,c1,c2) ->
-      let c1' = subst_pattern subst c1 in
-      let c2' = subst_pattern subst c2 in
+      let c1' = subst_pattern env sigma subst c1 in
+      let c2' = subst_pattern env sigma subst c2 in
 	if c1' == c1 && c2' == c2 then pat else
 	  PLambda (name,c1',c2')
   | PProd (name,c1,c2) ->
-      let c1' = subst_pattern subst c1 in
-      let c2' = subst_pattern subst c2 in
+      let c1' = subst_pattern env sigma subst c1 in
+      let c2' = subst_pattern env sigma subst c2 in
 	if c1' == c1 && c2' == c2 then pat else
 	  PProd (name,c1',c2')
   | PLetIn (name,c1,t,c2) ->
-      let c1' = subst_pattern subst c1 in
-      let t' = Option.Smart.map (subst_pattern subst) t in
-      let c2' = subst_pattern subst c2 in
+      let c1' = subst_pattern env sigma subst c1 in
+      let t' = Option.Smart.map (subst_pattern env sigma subst) t in
+      let c2' = subst_pattern env sigma subst c2 in
 	if c1' == c1 && t' == t && c2' == c2 then pat else
 	  PLetIn (name,c1',t',c2')
   | PSort _
   | PMeta _ -> pat
   | PIf (c,c1,c2) ->
-      let c' = subst_pattern subst c in
-      let c1' = subst_pattern subst c1 in
-      let c2' = subst_pattern subst c2 in
+      let c' = subst_pattern env sigma subst c in
+      let c1' = subst_pattern env sigma subst c1 in
+      let c2' = subst_pattern env sigma subst c2 in
 	if c' == c && c1' == c1 && c2' == c2 then pat else
 	  PIf (c',c1',c2')
   | PCase (cip,typ,c,branches) ->
       let ind = cip.cip_ind in
       let ind' = Option.Smart.map (subst_ind subst) ind in
       let cip' = if ind' == ind then cip else { cip with cip_ind = ind' } in
-      let typ' = subst_pattern subst typ in
-      let c' = subst_pattern subst c in
+      let typ' = subst_pattern env sigma subst typ in
+      let c' = subst_pattern env sigma subst c in
       let subst_branch ((i,n,c) as br) =
-	let c' = subst_pattern subst c in
+        let c' = subst_pattern env sigma subst c in
 	if c' == c then br else (i,n,c')
       in
       let branches' = List.Smart.map subst_branch branches in
@@ -347,13 +345,13 @@ let rec subst_pattern subst pat =
       then pat
       else PCase(cip', typ', c', branches')
   | PFix (lni,(lna,tl,bl)) ->
-      let tl' = Array.Smart.map (subst_pattern subst) tl in
-      let bl' = Array.Smart.map (subst_pattern subst) bl in
+      let tl' = Array.Smart.map (subst_pattern env sigma subst) tl in
+      let bl' = Array.Smart.map (subst_pattern env sigma subst) bl in
       if bl' == bl && tl' == tl then pat
       else PFix (lni,(lna,tl',bl'))
   | PCoFix (ln,(lna,tl,bl)) ->
-      let tl' = Array.Smart.map (subst_pattern subst) tl in
-      let bl' = Array.Smart.map (subst_pattern subst) bl in
+      let tl' = Array.Smart.map (subst_pattern env sigma subst) tl in
+      let bl' = Array.Smart.map (subst_pattern env sigma subst) bl in
       if bl' == bl && tl' == tl then pat
       else PCoFix (ln,(lna,tl',bl'))
 
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 36317b3acf..3821fbf1a0 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -21,7 +21,7 @@ val constr_pattern_eq : constr_pattern -> constr_pattern -> bool
 
 val occur_meta_pattern : constr_pattern -> bool
 
-val subst_pattern : substitution -> constr_pattern -> constr_pattern
+val subst_pattern : Environ.env -> Evd.evar_map -> substitution -> constr_pattern -> constr_pattern
 
 val noccurn_pattern : int -> constr_pattern -> bool
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a6e3cfe085..0f7676cd19 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -644,7 +644,7 @@ let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env
 	| None -> []
 	| Some ty ->
           let ((ind, i), u) = destConstruct sigma fj.uj_val in
-	  let npars = inductive_nparams ind in
+          let npars = inductive_nparams !!env ind in
 	    if Int.equal npars 0 then []
 	    else
 	      try
@@ -1146,7 +1146,7 @@ let understand_ltac flags env sigma lvar kind c =
   let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in
   (sigma, c)
 
-let path_convertible p q =
+let path_convertible env sigma p q =
   let open Classops in
   let mkGRef ref          = DAst.make @@ Glob_term.GRef(ref,None) in
   let mkGVar id           = DAst.make @@ Glob_term.GVar(id) in
@@ -1171,13 +1171,12 @@ let path_convertible p q =
     | [] -> anomaly (str "A coercion path shouldn't be empty.")
   in
   try
-    let e = Global.env () in
-    let sigma,tp = understand_tcc e (Evd.from_env e) (path_to_gterm p) in
-    let sigma,tq = understand_tcc e sigma (path_to_gterm q) in
+    let sigma,tp = understand_tcc env sigma (path_to_gterm p) in
+    let sigma,tq = understand_tcc env sigma (path_to_gterm q) in
     if Evd.has_undefined sigma then
       false
     else
-      let _ = Evarconv.unify_delay e sigma tp tq in true
+      let _ = Evarconv.unify_delay env sigma tp tq in true
   with Evarconv.UnableToUnify _ | PretypeError _ -> false
 
 let _ = Classops.install_path_comparator path_convertible
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index ef56458f99..1feb8acd5f 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -21,7 +21,6 @@ open Pp
 open Names
 open Globnames
 open Constr
-open Libobject
 open Mod_subst
 open Reductionops
 
@@ -50,10 +49,10 @@ let projection_table =
 type struc_tuple =
     constructor * (Name.t * bool) list * Constant.t option list
 
-let load_structure i (_, (id,kl,projs)) =
+let register_structure env (id,kl,projs) =
   let open Declarations in
   let ind = fst id in
-  let mib, mip = Global.lookup_inductive ind in
+  let mib, mip = Inductive.lookup_mind_specif env ind in
   let n = mib.mind_nparams in
   let struc =
     { s_CONST = id; s_EXPECTEDPARAM = n; s_PROJ = projs; s_PROJKIND = kl } in
@@ -62,10 +61,7 @@ let load_structure i (_, (id,kl,projs)) =
     List.fold_right (Option.fold_right (fun proj -> Cmap.add proj struc))
       projs !projection_table
 
-let cache_structure o =
-  load_structure 1 o
-
-let subst_structure (subst, (id, kl, projs as obj)) =
+let subst_structure subst (id, kl, projs as obj) =
   let projs' =
    (* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
    (* the first component of subst_con.                                   *)
@@ -77,19 +73,6 @@ let subst_structure (subst, (id, kl, projs as obj)) =
   if projs' == projs && id' == id then obj else
     (id',kl,projs')
 
-let discharge_structure (_, x) = Some x
-
-let inStruc : 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 o =
-  Lib.add_anonymous_leaf (inStruc o)
-
 let lookup_structure indsp = Indmap.find indsp !structure_table
 
 let lookup_projections indsp = (lookup_structure indsp).s_PROJ
@@ -107,26 +90,9 @@ let is_projection cst = Cmap.mem cst !projection_table
 let prim_table =
   Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs"
 
-let load_prim i (_,(p,c)) =
+let register_primitive_projection p c =
   prim_table := Cmap_env.add c p !prim_table
 
-let cache_prim p = load_prim 1 p
-
-let subst_prim (subst,(p,c)) = subst_proj_repr subst p, subst_constant subst c
-
-let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c)
-
-let inPrim : (Projection.Repr.t * Constant.t) -> obj =
-  declare_object {
-    (default_object "PRIMPROJS") with
-    cache_function = cache_prim ;
-    load_function = load_prim;
-    subst_function = subst_prim;
-    classify_function = (fun x -> Substitute x);
-    discharge_function = discharge_prim }
-
-let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c))
-
 let is_primitive_projection c = Cmap_env.mem c !prim_table
 
 let find_primitive_projection c =
@@ -224,7 +190,7 @@ let warn_projection_no_head_constant =
           ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.")
 
 (* Intended to always succeed *)
-let compute_canonical_projections env warn (con,ind) =
+let compute_canonical_projections env ~warn (con,ind) =
   let ctx = Environ.constant_context env con in
   let u = Univ.make_abstract_instance ctx in
   let v = (mkConstU (con,u)) in
@@ -274,11 +240,8 @@ let warn_redundant_canonical_projection =
           ++ strbrk " by " ++ prj ++ strbrk " in "
           ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s)
 
-let add_canonical_structure warn o =
-    (* XXX: Undesired global access to env *)
-    let env = Global.env () in
-    let sigma = Evd.from_env env in
-    compute_canonical_projections env warn o |>
+let register_canonical_structure ~warn env sigma o =
+    compute_canonical_projections env ~warn o |>
     List.iter (fun ((proj, (cs_pat, _ as pat)), s) ->
       let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
       match assoc_pat cs_pat l with
@@ -294,31 +257,13 @@ let add_canonical_structure warn o =
           warn_redundant_canonical_projection (hd_val, prj, new_can_s, old_can_s)
       )
 
-let open_canonical_structure i (_, o) =
-  if Int.equal i 1 then add_canonical_structure false o
-
-let cache_canonical_structure (_, o) =
-  add_canonical_structure true o
-
-let subst_canonical_structure (subst,(cst,ind as obj)) =
+let subst_canonical_structure subst (cst,ind as obj) =
   (* invariant: cst is an evaluable reference. Thus we can take *)
   (* the first component of subst_con.                                   *)
   let cst' = subst_constant subst cst in
   let ind' = subst_ind subst ind in
   if cst' == cst && ind' == ind then obj else (cst',ind')
 
-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 = subst_canonical_structure;
-    classify_function = (fun x -> Substitute x);
-    discharge_function = discharge_canonical_structure }
-
-let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
-
 (*s High-level declaration of a canonical structure *)
 
 let error_not_structure ref description =
@@ -327,20 +272,17 @@ let error_not_structure ref description =
        (Id.print (Nametab.basename_of_global ref) ++ str"." ++ spc() ++
           description))
 
-let check_and_decompose_canonical_structure ref =
+let check_and_decompose_canonical_structure env sigma ref =
   let sp =
     match ref with
       ConstRef sp -> sp
     |  _ -> error_not_structure ref (str "Expected an instance of a record or structure.")
   in
-  let env = Global.env () in
   let u = Univ.make_abstract_instance (Environ.constant_context env sp) in
   let vc = match Environ.constant_opt_value_in env (sp, u) with
     | Some vc -> vc
     | None -> error_not_structure ref (str "Could not find its value in the global environment.") in
-  let env = Global.env () in
-  let evd = Evd.from_env env in
-  let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in
+  let body = snd (splay_lam env sigma (EConstr.of_constr vc)) in
   let body = EConstr.Unsafe.to_constr body in
   let f,args = match kind body with
     | App (f,args) -> f,args
@@ -353,15 +295,12 @@ let check_and_decompose_canonical_structure ref =
     try lookup_structure indsp
     with Not_found ->
       error_not_structure ref
-        (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env evd (EConstr.mkInd indsp)) in
+        (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env sigma (EConstr.mkInd indsp)) in
   let ntrue_projs = List.count snd s.s_PROJKIND in
   if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then
     error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
   (sp,indsp)
 
-let declare_canonical_structure ref =
-  add_canonical_structure (check_and_decompose_canonical_structure ref)
-
 let lookup_canonical_conversion (proj,pat) =
   assoc_pat pat (GlobRef.Map.find proj !object_table)
 
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 53a33f6bab..f0594d513a 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -26,7 +26,8 @@ type struc_typ = {
 type struc_tuple =
     constructor * (Name.t * bool) list * Constant.t option list
 
-val declare_structure : struc_tuple -> unit
+val register_structure : Environ.env -> struc_tuple -> unit
+val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple
 
 (** [lookup_structure isp] returns the struc_typ associated to the
    inductive path [isp] if it corresponds to a structure, otherwise
@@ -47,7 +48,7 @@ val find_projection : GlobRef.t -> struc_typ
 val is_projection : Constant.t -> bool
 
 (** Sets up the mapping from constants to primitive projections *)
-val declare_primitive_projection : Projection.Repr.t -> Constant.t -> unit
+val register_primitive_projection : Projection.Repr.t -> Constant.t -> unit
 
 val is_primitive_projection : Constant.t -> bool
 
@@ -80,8 +81,12 @@ val cs_pattern_of_constr : Environ.env -> constr -> cs_pattern * int option * co
 val pr_cs_pattern : cs_pattern -> Pp.t
 
 val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ
-val declare_canonical_structure : GlobRef.t -> unit
+val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
+  Constant.t * inductive -> unit
+val subst_canonical_structure : Mod_subst.substitution -> Constant.t * inductive -> Constant.t * inductive
 val is_open_canonical_projection :
   Environ.env -> Evd.evar_map -> Reductionops.state -> bool
 val canonical_projections : unit ->
   ((GlobRef.t * cs_pattern) * obj_typ) list
+
+val check_and_decompose_canonical_structure : Environ.env -> Evd.evar_map -> GlobRef.t -> Constant.t * inductive
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 20120f4182..38e254a5b4 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -121,7 +121,7 @@ let retype ?(polyprop=true) sigma =
             Inductiveops.find_rectype env sigma t
           with Not_found -> retype_error BadRecursiveType
         in
-        let n = inductive_nrealdecls_env env (fst (fst (dest_ind_family indf))) in
+        let n = inductive_nrealdecls env (fst (fst (dest_ind_family indf))) in
         let t = betazetaevar_applist sigma n p realargs in
         (match EConstr.kind sigma (whd_all env sigma (type_of env t)) with
           | Prod _ -> whd_beta sigma (applist (t, [c]))
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 1496712bbc..ee27aea93f 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -17,11 +17,8 @@ open Vars
 open Evd
 open Util
 open Typeclasses_errors
-open Libobject
 open Context.Rel.Declaration
 
-module RelDecl = Context.Rel.Declaration
-module NamedDecl = Context.Named.Declaration
 (*i*)
 
 (* Core typeclasses hints *)
@@ -38,12 +35,6 @@ let get_typeclasses_unique_solutions =
     ~key:["Typeclasses";"Unique";"Solutions"]
     ~value:false
 
-let (add_instance_hint, add_instance_hint_hook) = Hook.make ()
-let add_instance_hint id = Hook.get add_instance_hint id
-
-let (remove_instance_hint, remove_instance_hint_hook) = Hook.make ()
-let remove_instance_hint id = Hook.get remove_instance_hint id
-
 let (set_typeclass_transparency, set_typeclass_transparency_hook) = Hook.make ()
 let set_typeclass_transparency gr local c = Hook.get set_typeclass_transparency gr local c
 
@@ -97,18 +88,6 @@ let instance_impl is = is.is_impl
 
 let hint_priority is = is.is_info.hint_priority
 
-let new_instance cl info glob impl =
-  let global =
-    if glob then Some (Lib.sections_depth ())
-    else None
-  in
-  if match global with Some n -> n>0 && isVarRef impl | _ -> false then
-    CErrors.user_err (Pp.str "Cannot set Global an instance referring to a section variable.");
-    { is_class = cl.cl_impl;
-      is_info = info ;
-      is_global = global ;
-      is_impl = impl }
-
 (*
  * states management
  *)
@@ -122,11 +101,10 @@ let typeclass_univ_instance (cl, u) =
     { cl with cl_context = on_snd subst_ctx cl.cl_context;
       cl_props = subst_ctx cl.cl_props}
 
-let class_info c =
+let class_info env sigma c =
   try GlobRef.Map.find c !classes
   with Not_found ->
-    let env = Global.env() in
-    not_a_class env (Evd.from_env env) (EConstr.of_constr (printable_constr_of_global c))
+    not_a_class env sigma (EConstr.of_constr (printable_constr_of_global c))
 
 let global_class_of_constr env sigma c =
   try let gr, u = Termops.global_of_constr sigma c in
@@ -142,8 +120,8 @@ let dest_class_arity env sigma c =
   let rels, c = decompose_prod_assum sigma c in
     rels, dest_class_app env sigma c
 
-let class_of_constr sigma c =
-  try Some (dest_class_arity (Global.env ()) sigma c)
+let class_of_constr env sigma c =
+  try Some (dest_class_arity env sigma c)
   with e when CErrors.noncritical e -> None
 
 let is_class_constr sigma c = 
@@ -176,103 +154,9 @@ let rec is_maybe_class_type evd c =
 
 let () = Hook.set Evd.is_maybe_typeclass_hook (fun evd c -> is_maybe_class_type evd (EConstr.of_constr c))
 
-(*
- * classes persistent object
- *)
-
-let load_class (_, cl) =
+let load_class cl =
   classes := GlobRef.Map.add cl.cl_impl cl !classes
 
-let cache_class = load_class
-
-let subst_class (subst,cl) =
-  let do_subst_con c = Mod_subst.subst_constant subst c
-  and do_subst c = Mod_subst.subst_mps subst c
-  and do_subst_gr gr = fst (subst_global subst gr) in
-  let do_subst_ctx = List.Smart.map (RelDecl.map_constr do_subst) in
-  let do_subst_context (grs,ctx) =
-    List.Smart.map (Option.Smart.map do_subst_gr) grs,
-    do_subst_ctx ctx in
-  let do_subst_projs projs = List.Smart.map (fun (x, y, z) ->
-    (x, y, Option.Smart.map do_subst_con z)) projs in
-  { cl_univs = cl.cl_univs;
-    cl_impl = do_subst_gr cl.cl_impl;
-    cl_context = do_subst_context cl.cl_context;
-    cl_props = do_subst_ctx cl.cl_props;
-    cl_projs = do_subst_projs cl.cl_projs;
-    cl_strict = cl.cl_strict;
-    cl_unique = cl.cl_unique }
-
-let discharge_class (_,cl) =
-  let repl = Lib.replacement_context () in
-  let rel_of_variable_context ctx = List.fold_right
-    ( fun (decl,_) (ctx', subst) ->
-        let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel_decl in
-	(decl' :: ctx', NamedDecl.get_id decl :: subst)
-    ) ctx ([], []) in
-  let discharge_rel_context (subst, usubst) n rel =
-    let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
-    let fold decl (ctx, k) =
-      let map c = subst_univs_level_constr usubst (substn_vars k subst c) in
-      RelDecl.map_constr map decl :: ctx, succ k
-    in
-    let ctx, _ = List.fold_right fold rel ([], n) in
-    ctx
-  in
-  let abs_context cl =
-    match cl.cl_impl with
-      | VarRef _ | ConstructRef _ -> assert false
-      | ConstRef cst -> Lib.section_segment_of_constant cst
-      | IndRef (ind,_) -> Lib.section_segment_of_mutual_inductive ind in
-  let discharge_context ctx' subst (grs, ctx) =
-    let grs' =
-      let newgrs = List.map (fun decl ->
-			     match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr Evd.empty with
-			     | None -> None
-                             | Some (_, ((tc,_), _)) -> Some tc.cl_impl)
-			    ctx'
-      in
-      grs @ newgrs
-    in grs', discharge_rel_context subst 1 ctx @ ctx' in
-  try
-    let info = abs_context cl in
-    let ctx = info.Lib.abstr_ctx in
-    let ctx, subst = rel_of_variable_context ctx in
-    let usubst, cl_univs' = Lib.discharge_abstract_universe_context info cl.cl_univs in
-    let context = discharge_context ctx (subst, usubst) cl.cl_context in
-    let props = discharge_rel_context (subst, usubst) (succ (List.length (fst cl.cl_context))) cl.cl_props in
-    let discharge_proj x = x in
-    { cl_univs = cl_univs';
-      cl_impl = cl.cl_impl;
-      cl_context = context;
-      cl_props = props;
-      cl_projs = List.Smart.map discharge_proj cl.cl_projs;
-      cl_strict = cl.cl_strict;
-      cl_unique = cl.cl_unique
-    }
-  with Not_found -> (* not defined in the current section *)
-    cl
-
-let rebuild_class cl = 
-  try 
-    let cst = Tacred.evaluable_of_global_reference (Global.env ()) cl.cl_impl in
-      set_typeclass_transparency cst false false; cl
-  with e when CErrors.noncritical e -> cl
-
-let class_input : typeclass -> obj =
-  declare_object
-    { (default_object "type classes state") with
-      cache_function = cache_class;
-      load_function = (fun _ -> load_class);
-      open_function = (fun _ -> load_class);
-      classify_function = (fun x -> Substitute x);
-      discharge_function = (fun a -> Some (discharge_class a));
-      rebuild_function = rebuild_class;
-      subst_function = subst_class }
-
-let add_class cl =
-  Lib.add_anonymous_leaf (class_input cl)
-
 (** Build the subinstances hints. *)
 
 let check_instance env sigma c =
@@ -295,7 +179,7 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
   let ty = EConstr.of_constr ty in
   let sigma = Evd.merge_context_set Evd.univ_rigid sigma ctx in
   let rec aux pri c ty path =
-      match class_of_constr sigma ty with
+      match class_of_constr env sigma ty with
       | None -> []
       | Some (rels, ((tc,u), args)) ->
 	let instapp = 
@@ -336,136 +220,23 @@ let build_subclasses ~check env sigma glob { hint_priority = pri } =
     aux pri term ty [glob]
 
 (*
- * instances persistent object
+ * interface functions
  *)
 
-type instance_action = 
-  | AddInstance
-  | RemoveInstance
-
-let load_instance inst = 
-  let insts = 
+let load_instance inst =
+  let insts =
     try GlobRef.Map.find inst.is_class !instances
     with Not_found -> GlobRef.Map.empty in
   let insts = GlobRef.Map.add inst.is_impl inst insts in
   instances := GlobRef.Map.add inst.is_class insts !instances
 
 let remove_instance inst =
-  let insts = 
+  let insts =
     try GlobRef.Map.find inst.is_class !instances
     with Not_found -> assert false in
   let insts = GlobRef.Map.remove inst.is_impl insts in
   instances := GlobRef.Map.add inst.is_class insts !instances
 
-let cache_instance (_, (action, i)) =
-  match action with 
-  | AddInstance -> load_instance i
-  | RemoveInstance -> remove_instance i      
-
-let subst_instance (subst, (action, inst)) = action,
-  { inst with 
-      is_class = fst (subst_global subst inst.is_class);
-      is_impl = fst (subst_global subst inst.is_impl) }
-
-let discharge_instance (_, (action, inst)) =
-  match inst.is_global with
-  | None -> None
-  | Some n ->
-    assert (not (isVarRef inst.is_impl));
-    Some (action,
-    { inst with 
-      is_global = Some (pred n);
-      is_class = inst.is_class;
-      is_impl = inst.is_impl })
-    
-
-let is_local i = (i.is_global == None)
-
-let is_local_for_hint i =
-  match i.is_global with
-  | None -> true  (* i.e. either no Global keyword not in section, or in section *)
-  | Some n -> n <> 0 (* i.e. in a section, declare the hint as local
-     since discharge is managed by rebuild_instance which calls again
-     add_instance_hint; don't ask hints to take discharge into account
-     itself *)
-
-let add_instance check inst =
-  let poly = Global.is_polymorphic inst.is_impl in
-  let local = is_local_for_hint inst in
-  add_instance_hint (IsGlobal inst.is_impl) [inst.is_impl] local
-    inst.is_info poly;
-  List.iter (fun (path, pri, c) -> add_instance_hint (IsConstr c) path
-    local pri poly)
-    (build_subclasses ~check:(check && not (isVarRef inst.is_impl))
-       (Global.env ()) (Evd.from_env (Global.env ())) inst.is_impl inst.is_info)
-
-let rebuild_instance (action, inst) =
-  let () = match action with
-  | AddInstance -> add_instance true inst
-  | _ -> ()
-  in
-  (action, inst)
-
-let classify_instance (action, inst) =
-  if is_local inst then Dispose
-  else Substitute (action, inst)
-
-let instance_input : instance_action * instance -> obj =
-  declare_object
-    { (default_object "type classes instances state") with
-      cache_function = cache_instance;
-      load_function = (fun _ x -> cache_instance x);
-      open_function = (fun _ x -> cache_instance x);
-      classify_function = classify_instance;
-      discharge_function = discharge_instance;
-      rebuild_function = rebuild_instance;
-      subst_function = subst_instance }
-
-let add_instance i =
-  Lib.add_anonymous_leaf (instance_input (AddInstance, i));
-  add_instance true i
-
-let remove_instance i =
-  Lib.add_anonymous_leaf (instance_input (RemoveInstance, i));
-  remove_instance_hint i.is_impl
-
-let warning_not_a_class =
-  let name = "not-a-class" in
-  let category = "typeclasses" in
-  CWarnings.create ~name ~category (fun (n, ty) ->
-      let env = Global.env () in
-      let evd = Evd.from_env env in
-      Pp.(str "Ignored instance declaration for “"
-          ++ Nametab.pr_global_env Id.Set.empty n
-          ++ str "”: “"
-          ++ Termops.Internal.print_constr_env env evd (EConstr.of_constr ty)
-          ++ str "” is not a class")
-    )
-
-let declare_instance ?(warn = false) info local glob =
-  let ty, _ = Typeops.type_of_global_in_context (Global.env ()) glob in
-  let info = Option.default {hint_priority = None; hint_pattern = None} info in
-    match class_of_constr Evd.empty (EConstr.of_constr ty) with
-    | Some (rels, ((tc,_), args) as _cl) ->
-      assert (not (isVarRef glob) || local);
-      add_instance (new_instance tc info (not local) glob)
-    | None -> if warn then warning_not_a_class (glob, ty)
-
-let add_class cl =
-  add_class cl;
-  List.iter (fun (n, inst, body) ->
-      match inst with
-      | Some (Backward, info) ->
-        (match body with
-         | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance")
-         | Some b -> declare_instance ~warn:true (Some info) false (ConstRef b))
-      | _ -> ())
-    cl.cl_projs
-
-
-(*
- * interface functions
- *)
 
 let instance_constructor (cl,u) args =
   let lenpars = List.count is_local_assum (snd cl.cl_context) in
@@ -497,8 +268,8 @@ let all_instances () =
     GlobRef.Map.fold (fun k v acc -> v :: acc) v acc)
     !instances []
 
-let instances r = 
-  let cl = class_info r in instances_of cl    
+let instances env sigma r =
+  let cl = class_info env sigma r in instances_of cl
 
 let is_class gr = 
   GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index f8aedf88c2..e42b82c51f 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Globnames
 open Constr
 open Evd
 open Environ
@@ -54,19 +53,25 @@ type typeclass = {
       no backtracking and sharing of resolution. *)
 }
 
-type instance
+type instance = {
+  is_class: GlobRef.t;
+  is_info: hint_info;
+  (* Sections where the instance should be redeclared,
+     None for discard, Some 0 for none. *)
+  is_global: int option;
+  is_impl: GlobRef.t;
+}
 
-val instances : GlobRef.t -> instance list
+val instances : env -> evar_map -> GlobRef.t -> instance list
 val typeclasses : unit -> typeclass list
 val all_instances : unit -> instance list
 
-val add_class : typeclass -> unit
+val load_class : typeclass -> unit
 
-val new_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance
-val add_instance : instance -> unit
+val load_instance : instance -> unit
 val remove_instance : instance -> unit
 
-val class_info : GlobRef.t -> typeclass (** raises a UserError if not a class *)
+val class_info : env -> evar_map -> GlobRef.t -> typeclass (** raises a UserError if not a class *)
 
 
 (** These raise a UserError if not a class.
@@ -78,7 +83,8 @@ val dest_class_app : env -> evar_map -> EConstr.constr -> (typeclass * EConstr.E
 val typeclass_univ_instance : typeclass Univ.puniverses -> typeclass
 
 (** Just return None if not a class *)
-val class_of_constr : evar_map -> EConstr.constr -> (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option
+val class_of_constr : env -> evar_map -> EConstr.constr ->
+  (EConstr.rel_context * ((typeclass * EConstr.EInstance.t) * constr list)) option
 
 val instance_impl : instance -> GlobRef.t
 
@@ -122,23 +128,9 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
 val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t
 val classes_transparent_state : unit -> TransparentState.t
 
-val add_instance_hint_hook :
-  (global_reference_or_constr -> GlobRef.t list ->
-   bool (* local? *) -> hint_info -> Decl_kinds.polymorphic -> unit) Hook.t
-val remove_instance_hint_hook : (GlobRef.t -> unit) Hook.t
-val add_instance_hint : global_reference_or_constr -> GlobRef.t list ->
-  bool -> hint_info -> Decl_kinds.polymorphic -> unit
-val remove_instance_hint : GlobRef.t -> unit
-
 val solve_all_instances_hook : (env -> evar_map -> evar_filter -> bool -> bool -> bool -> evar_map) Hook.t
 val solve_one_instance_hook : (env -> evar_map -> EConstr.types -> bool -> evar_map * EConstr.constr) Hook.t
 
-(** Declares the given global reference as an instance of its type.
-    Does nothing — or emit a “not-a-class” warning if the [warn] argument is set —
-    when said type is not a registered type class. *)
-val declare_instance : ?warn:bool -> hint_info option -> bool -> GlobRef.t -> unit
-
-
 (** Build the subinstances hints for a given typeclass object.
     check tells if we should check for existence of the 
     subinstances and add only the missing ones. *)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 89f72c874b..be71f44a5e 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -198,7 +198,7 @@ let check_type_fixpoint ?loc env sigma lna lar vdefj =
 
 (* FIXME: might depend on the level of actual parameters!*)
 let check_allowed_sort env sigma ind c p =
-  let specif = Global.lookup_inductive (fst ind) in
+  let specif = lookup_mind_specif env (fst ind) in
   let sorts = elim_sorts specif in
   let pj = Retyping.get_judgment_of env sigma p in
   let _, s = splay_prod env sigma pj.uj_type in