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

68 files changed, 1071 insertions, 979 deletions

diff --git a/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh
new file mode 100644
index 0000000000..01d3068591
--- /dev/null
+++ b/dev/ci/user-overlays/09909-maximedenes-pretyping-rm-global.sh
@@ -0,0 +1,21 @@
+if [ "$CI_PULL_REQUEST" = "9909" ] || [ "$CI_BRANCH" = "pretyping-rm-global" ]; then
+
+    elpi_CI_REF=pretyping-rm-global
+    elpi_CI_GITURL=https://github.com/maximedenes/coq-elpi
+
+    coqhammer_CI_REF=pretyping-rm-global
+    coqhammer_CI_GITURL=https://github.com/maximedenes/coqhammer
+
+    equations_CI_REF=pretyping-rm-global
+    equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+
+    ltac2_CI_REF=pretyping-rm-global
+    ltac2_CI_GITURL=https://github.com/maximedenes/ltac2
+
+    paramcoq_CI_REF=pretyping-rm-global
+    paramcoq_CI_GITURL=https://github.com/maximedenes/paramcoq
+
+    mtac2_CI_REF=pretyping-rm-global
+    mtac2_CI_GITURL=https://github.com/maximedenes/Mtac2
+
+fi
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 24b1362e6d..b89b6b5765 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -212,7 +212,7 @@ let encode_record r =
 
 module PrintingRecordRecord =
   PrintingInductiveMake (struct
-    let encode = encode_record
+    let encode _env = encode_record
     let field = "Record"
     let title = "Types leading to pretty-printing using record notation: "
     let member_message s b =
@@ -224,7 +224,7 @@ module PrintingRecordRecord =
 
 module PrintingRecordConstructor =
   PrintingInductiveMake (struct
-    let encode = encode_record
+    let encode _env = encode_record
     let field = "Constructor"
     let title = "Types leading to pretty-printing using constructor form: "
     let member_message s b =
@@ -289,11 +289,11 @@ let extern_reference ?loc vars l = !my_extern_reference vars l
 
 let add_patt_for_params ind l =
   if !Flags.in_debugger then l else
-    Util.List.addn (Inductiveops.inductive_nparamdecls ind) (CAst.make @@ CPatAtom None) l
+    Util.List.addn (Inductiveops.inductive_nparamdecls (Global.env()) ind) (CAst.make @@ CPatAtom None) l
 
 let add_cpatt_for_params ind l =
   if !Flags.in_debugger then l else
-    Util.List.addn  (Inductiveops.inductive_nparamdecls ind) (DAst.make @@ PatVar Anonymous) l
+    Util.List.addn  (Inductiveops.inductive_nparamdecls (Global.env()) ind) (DAst.make @@ PatVar Anonymous) l
 
 let drop_implicits_in_patt cst nb_expl args =
   let impl_st = (implicits_of_global cst) in
@@ -364,7 +364,7 @@ let mkPat ?loc qid l = CAst.make ?loc @@
 
 let pattern_printable_in_both_syntax (ind,_ as c) =
   let impl_st = extract_impargs_data (implicits_of_global (ConstructRef c)) in
-  let nb_params = Inductiveops.inductive_nparams ind in
+  let nb_params = Inductiveops.inductive_nparams (Global.env()) ind in
   List.exists (fun (_,impls) ->
     (List.length impls >= nb_params) &&
       let params,args = Util.List.chop nb_params impls in
@@ -526,7 +526,7 @@ let rec extern_notation_ind_pattern allscopes lonely_seen vars ind args = functi
 let extern_ind_pattern_in_scope (custom,scopes as allscopes) vars ind args =
   (* pboutill: There are letins in pat which is incompatible with notations and
      not explicit application. *)
-  if !Flags.in_debugger||Inductiveops.inductive_has_local_defs ind then
+  if !Flags.in_debugger||Inductiveops.inductive_has_local_defs (Global.env()) ind then
     let c = extern_reference vars (IndRef ind) in
     let args = List.map (extern_cases_pattern_in_scope allscopes vars) args in
     CAst.make @@ CPatCstr (c, Some (add_patt_for_params ind args), [])
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 749eb2289c..3329ba2047 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -643,7 +643,7 @@ let terms_of_binders bl =
     | PatCstr (c,l,_) ->
        let qid = qualid_of_path ?loc (Nametab.path_of_global (ConstructRef c)) in
        let hole = CAst.make ?loc @@ CHole (None,IntroAnonymous,None) in
-       let params = List.make (Inductiveops.inductive_nparams (fst c)) hole in
+       let params = List.make (Inductiveops.inductive_nparams (Global.env()) (fst c)) hole in
        CAppExpl ((None,qid,None),params @ List.map term_of_pat l)) pt in
   let rec extract_variables l = match l with
     | bnd :: l ->
@@ -738,7 +738,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
           else
             let _,((disjpat,_),_),_ = intern_pat ntnvars nenv c in
             match disjpat with
-            | [pat] -> (glob_constr_of_cases_pattern pat, None)
+            | [pat] -> (glob_constr_of_cases_pattern (Global.env()) pat, None)
             | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc ()
         in
         let terms = Id.Map.fold mk_env terms Id.Map.empty in
@@ -800,7 +800,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
       else
         let env,((disjpat,ids),id),na = intern_pat ntnvars env pat in
         match disjpat with
-        | [pat] -> glob_constr_of_cases_pattern pat
+        | [pat] -> glob_constr_of_cases_pattern (Global.env()) pat
         | _ -> user_err Pp.(str "Cannot turn a disjunctive pattern into a term.")
     with Not_found ->
     try
@@ -1197,10 +1197,10 @@ let check_or_pat_variables loc ids idsl =
     @return if letin are included *)
 let check_constructor_length env loc cstr len_pl pl0 =
   let n = len_pl + List.length pl0 in
-  if Int.equal n (Inductiveops.constructor_nallargs cstr) then false else
-    (Int.equal n (Inductiveops.constructor_nalldecls cstr) ||
+  if Int.equal n (Inductiveops.constructor_nallargs env cstr) then false else
+    (Int.equal n (Inductiveops.constructor_nalldecls env cstr) ||
       (error_wrong_numarg_constructor ?loc env cstr
-         (Inductiveops.constructor_nrealargs cstr)))
+         (Inductiveops.constructor_nrealargs env cstr)))
 
 open Declarations
 
@@ -1226,9 +1226,9 @@ let add_local_defs_and_check_length loc env g pl args = match g with
         have been given in the "explicit" arguments, which come from a
         "@C args" notation or from a custom user notation *)
      let pl' = insert_local_defs_in_pattern cstr pl in
-     let maxargs = Inductiveops.constructor_nalldecls cstr in
+     let maxargs = Inductiveops.constructor_nalldecls env cstr in
      if List.length pl' + List.length args > maxargs then
-       error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr);
+       error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs env cstr);
      (* Two possibilities: either the args are given with explict
      variables for local definitions, then we give the explicit args
      extended with local defs, so that there is nothing more to be
@@ -1258,15 +1258,15 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
   in aux 0 (impl_list,pl2)
 
 let add_implicits_check_constructor_length env loc c len_pl1 pl2 =
-  let nargs = Inductiveops.constructor_nallargs c in
-  let nargs' = Inductiveops.constructor_nalldecls c in
+  let nargs = Inductiveops.constructor_nallargs env c in
+  let nargs' = Inductiveops.constructor_nalldecls env c in
   let impls_st = implicits_of_global (ConstructRef c) in
   add_implicits_check_length (error_wrong_numarg_constructor ?loc env c)
     nargs nargs' impls_st len_pl1 pl2
 
 let add_implicits_check_ind_length env loc c len_pl1 pl2 =
-  let nallargs = inductive_nallargs_env env c in
-  let nalldecls = inductive_nalldecls_env env c in
+  let nallargs = inductive_nallargs env c in
+  let nalldecls = inductive_nalldecls env c in
   let impls_st = implicits_of_global (IndRef c) in
   add_implicits_check_length (error_wrong_numarg_inductive ?loc env c)
     nallargs nalldecls impls_st len_pl1 pl2
@@ -1274,8 +1274,8 @@ let add_implicits_check_ind_length env loc c len_pl1 pl2 =
 (** Do not raise NotEnoughArguments thanks to preconditions*)
 let chop_params_pattern loc ind args with_letin =
   let nparams = if with_letin
-    then Inductiveops.inductive_nparamdecls ind
-    else Inductiveops.inductive_nparams ind in
+    then Inductiveops.inductive_nparamdecls (Global.env()) ind
+    else Inductiveops.inductive_nparams (Global.env()) ind in
   assert (nparams <= List.length args);
   let params,args = List.chop nparams args in
   List.iter (fun c -> match DAst.get c with
@@ -1295,10 +1295,11 @@ let find_constructor loc add_params ref =
   in
   cstr, match add_params with
     | Some nb_args ->
+      let env = Global.env () in
       let nb =
-        if Int.equal nb_args (Inductiveops.constructor_nrealdecls cstr)
-          then Inductiveops.inductive_nparamdecls ind
-          else Inductiveops.inductive_nparams ind
+        if Int.equal nb_args (Inductiveops.constructor_nrealdecls env cstr)
+        then Inductiveops.inductive_nparamdecls env ind
+        else Inductiveops.inductive_nparams env ind
       in
       List.make nb ([], [(Id.Map.empty, DAst.make @@ PatVar Anonymous)])
     | None -> []
diff --git a/interp/declare.ml b/interp/declare.ml
index 717f8ef49a..76b4bab2ce 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -346,6 +346,25 @@ let inInductive : mutual_inductive_entry -> obj =
     discharge_function = discharge_inductive;
     rebuild_function = rebuild_inductive }
 
+let cache_prim (_,(p,c)) = Recordops.register_primitive_projection p c
+
+let load_prim _ p = cache_prim p
+
+let subst_prim (subst,(p,c)) = Mod_subst.subst_proj_repr subst p, Mod_subst.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 declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
   let id = Label.to_id label in
   let univs, u = match univs with
@@ -360,7 +379,7 @@ let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (ter
   let entry = definition_entry ~types ~univs term in
   let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
   let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
-  Recordops.declare_primitive_projection p cst
+  declare_primitive_projection p cst
 
 
 let declare_projections univs mind =
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 854651e7b7..dffccf02fc 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -231,23 +231,25 @@ let implicit_application env ?(allow_partial=true) f ty =
     | Some ({CAst.loc;v=(id, par, inst)}, gr) ->
 	let avoid = Id.Set.union env (ids_of_list (free_vars_of_constr_expr ty ~bound:env [])) in
 	let c, avoid =
-	  let c = class_info gr in
-	  let (ci, rd) = c.cl_context in
-	  if not allow_partial then
-	    begin
-              let opt_succ x n = match x with
-              | None -> succ n
-              | Some _ -> n
-              in
-	      let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
-	      let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
-		if not (Int.equal needlen applen) then
-                  mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
-	    end;
-	  let pars = List.rev (List.combine ci rd) in
-	  let args, avoid = combine_params avoid f par pars in
-	    CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
-	in c, avoid
+   let env = Global.env () in
+   let sigma = Evd.from_env env in
+   let c = class_info env sigma gr in
+   let (ci, rd) = c.cl_context in
+   if not allow_partial then
+     begin
+       let opt_succ x n = match x with
+         | None -> succ n
+         | Some _ -> n
+       in
+       let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
+       let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
+       if not (Int.equal needlen applen) then
+         mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
+     end;
+   let pars = List.rev (List.combine ci rd) in
+   let args, avoid = combine_params avoid f par pars in
+   CAst.make ?loc @@ CAppExpl ((None, id, inst), args), avoid
+ in c, avoid
 
 let warn_ignoring_implicit_status =
   CWarnings.create ~name:"ignoring_implicit_status" ~category:"implicits"
diff --git a/interp/notation.ml b/interp/notation.ml
index b9aca82cf4..56504db04e 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1516,7 +1516,7 @@ let uninterp_prim_token c =
      with Not_found -> raise Notation_ops.No_match
 
 let uninterp_prim_token_cases_pattern c =
-  match glob_constr_of_closed_cases_pattern c with
+  match glob_constr_of_closed_cases_pattern (Global.env()) c with
   | exception Not_found -> raise Notation_ops.No_match
   | na,c -> let (sc,n) = uninterp_prim_token c in (na,sc,n)
 
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7d7e10a05b..9801e56ca1 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -782,7 +782,7 @@ let rec pat_binder_of_term t = DAst.map (function
   | GApp (t, l) ->
     begin match DAst.get t with
     | GRef (ConstructRef cstr,_) ->
-     let nparams = Inductiveops.inductive_nparams (fst cstr) in
+     let nparams = Inductiveops.inductive_nparams (Global.env()) (fst cstr) in
      let _,l = List.chop nparams l in
      PatCstr (cstr, List.map pat_binder_of_term l, Anonymous)
     | _ -> raise No_match
@@ -909,7 +909,8 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma)
     alp, add_env alp sigma var (DAst.make @@ GVar id)
 
 let bind_binding_as_term_env alp (terms,termlists,binders,binderlists as sigma) var c =
-  let pat = try cases_pattern_of_glob_constr Anonymous c with Not_found -> raise No_match in
+  let env = Global.env () in
+  let pat = try cases_pattern_of_glob_constr env Anonymous c with Not_found -> raise No_match in
   try
     (* If already bound to a binder, unify the term and the binder *)
     let patl' = Id.List.assoc var binders in
@@ -1292,7 +1293,7 @@ let match_notation_constr u c (metas,pat) =
     | NtnTypeBinder (NtnBinderParsedAsConstr _) ->
        (match Id.List.assoc x binders with
         | [pat] ->
-          let v = glob_constr_of_cases_pattern pat in
+          let v = glob_constr_of_cases_pattern (Global.env()) pat in
           ((v,scl)::terms',termlists',binders',binderlists')
         | _ -> raise No_match)
     | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _) ->
@@ -1333,11 +1334,11 @@ let rec match_cases_pattern metas (terms,termlists,(),() as sigma) a1 a2 =
   | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
   | PatVar Anonymous, NHole _ -> sigma,(0,[])
   | PatCstr ((ind,_ as r1),largs,Anonymous), NRef (ConstructRef r2) when eq_constructor r1 r2 ->
-      let l = try add_patterns_for_params_remove_local_defs r1 largs with Not_found -> raise No_match in
+      let l = try add_patterns_for_params_remove_local_defs (Global.env ()) r1 largs with Not_found -> raise No_match in
       sigma,(0,l)
   | PatCstr ((ind,_ as r1),args1,Anonymous), NApp (NRef (ConstructRef r2),l2)
       when eq_constructor r1 r2 ->
-      let l1 = try add_patterns_for_params_remove_local_defs r1 args1 with Not_found -> raise No_match in
+      let l1 = try add_patterns_for_params_remove_local_defs (Global.env()) r1 args1 with Not_found -> raise No_match in
       let le2 = List.length l2 in
       if Int.equal le2 0 (* Special case of a notation for a @Cstr *) || le2 > List.length l1
       then
diff --git a/library/goptions.ml b/library/goptions.ml
index 1b907fd966..b9c1802a72 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -57,7 +57,7 @@ module MakeTable =
 	  type key
 	  val compare : t -> t -> int
 	  val table : (string * key table_of_A) list ref
-	  val encode : key -> t
+          val encode : Environ.env -> key -> t
 	  val subst : substitution -> t -> t
           val printer : t -> Pp.t
           val key : option_name
@@ -111,10 +111,10 @@ module MakeTable =
 
     class table_of_A () =
     object
-      method add x = add_option (A.encode x)
-      method remove x = remove_option (A.encode x)
+      method add x = add_option (A.encode (Global.env()) x)
+      method remove x = remove_option (A.encode (Global.env()) x)
       method mem x =
-	let y = A.encode x in
+        let y = A.encode (Global.env()) x in
         let answer = MySet.mem y !t in
         Feedback.msg_info (A.member_message y answer)
       method print = print_table A.title A.printer !t
@@ -142,7 +142,7 @@ struct
   type key = string
   let compare = String.compare
   let table = string_table
-  let encode x = x
+  let encode _env x = x
   let subst _ x = x
   let printer = str
   let key = A.key
@@ -161,7 +161,7 @@ module type RefConvertArg =
 sig
   type t
   val compare : t -> t -> int
-  val encode : qualid -> t
+  val encode : Environ.env -> qualid -> t
   val subst : substitution -> t -> t
   val printer : t -> Pp.t
   val key : option_name
diff --git a/library/goptions.mli b/library/goptions.mli
index b91553bf3c..9925eb9e7b 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -89,8 +89,8 @@ module MakeRefTable :
     (A : sig
            type t
            val compare : t -> t -> int
-           val encode : qualid -> t
-	   val subst : substitution -> t -> t
+           val encode : Environ.env -> qualid -> t
+           val subst : substitution -> t -> t
            val printer : t -> Pp.t
            val key : option_name
            val title : string
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 50fc2448fc..0e3b9fc2b6 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -67,7 +67,7 @@ let rec decompose_term env sigma t=
 	let canon_mind = MutInd.make1 (MutInd.canonical mind) in
 	let canon_ind = canon_mind,i_ind in
 	let (oib,_)=Global.lookup_inductive (canon_ind) in
-	let nargs=constructor_nallargs_env env (canon_ind,i_con) in
+        let nargs=constructor_nallargs env (canon_ind,i_con) in
 	  Constructor {ci_constr= ((canon_ind,i_con),u);
 		       ci_arity=nargs;
 		       ci_nhyps=nargs-oib.mind_nparams}
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index c9cfd74362..9db7c8d8d3 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -854,7 +854,7 @@ and extract_cons_app env sg mle mlt (((kn,i) as ip,j) as cp) args =
 and extract_case env sg mle ((kn,i) as ip,c,br) mlt =
   (* [br]: bodies of each branch (in functional form) *)
   (* [ni]: number of arguments without parameters in each branch *)
-  let ni = constructors_nrealargs_env env ip in
+  let ni = constructors_nrealargs env ip in
   let br_size = Array.length br in
   assert (Int.equal (Array.length ni) br_size);
   if Int.equal br_size 0 then begin
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 56b3dc97cf..4b7bc707d6 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -82,13 +82,13 @@ let pop t = Vars.lift (-1) t
 let kind_of_formula env sigma term =
   let normalize = special_nf env sigma in
   let cciterm = special_whd env sigma term in
-    match match_with_imp_term sigma cciterm with
+    match match_with_imp_term env sigma cciterm with
 	Some (a,b)-> Arrow (a, pop b)
       |_->
-	 match match_with_forall_term sigma cciterm with
+         match match_with_forall_term env sigma cciterm with
 	     Some (_,a,b)-> Forall (a, b)
 	   |_->
-	      match match_with_nodep_ind sigma cciterm with
+              match match_with_nodep_ind env sigma cciterm with
 		  Some (i,l,n)->
 		    let ind,u=EConstr.destInd sigma i in
 		    let u = EConstr.EInstance.kind sigma u in
@@ -111,7 +111,7 @@ let kind_of_formula env sigma term =
 			    else
 			      Or((ind,u),l,is_trivial)
 		| _ ->
-		    match match_with_sigma_type sigma cciterm with
+                    match match_with_sigma_type env sigma cciterm with
 			Some (i,l)->
                           let (ind, u) = EConstr.destInd sigma i in
                           let u = EConstr.EInstance.kind sigma u in
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 01b18e2f30..9f2ceb2c28 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -188,7 +188,7 @@ let empty_seq depth=
 let expand_constructor_hints =
   List.map_append (function
     | GlobRef.IndRef ind ->
-        List.init (Inductiveops.nconstructors ind)
+        List.init (Inductiveops.nconstructors (Global.env()) ind)
           (fun i -> GlobRef.ConstructRef (ind,i+1))
     | gr ->
 	[gr])
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 275b58f0aa..45a4e61846 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -317,7 +317,7 @@ let build_constructors_of_type ind' argl =
 		  Impargs.implicits_of_global constructref
 		in
 		let cst_narg =
-		  Inductiveops.constructor_nallargs_env
+                  Inductiveops.constructor_nallargs
 		    (Global.env ())
 		    construct
 		in
@@ -330,7 +330,7 @@ let build_constructors_of_type ind' argl =
 		let pat_as_term =
 		  mkGApp(mkGRef (ConstructRef(ind',i+1)),argl)
 		in
-		cases_pattern_of_glob_constr Anonymous pat_as_term
+                cases_pattern_of_glob_constr (Global.env()) Anonymous pat_as_term
 	     )
     ind.Declarations.mind_consnames
 
@@ -415,7 +415,7 @@ let rec pattern_to_term_and_type env typ  = DAst.with_val (function
 	mkGVar id
   | PatCstr(constr,patternl,_) ->
       let cst_narg =
-	Inductiveops.constructor_nallargs_env
+        Inductiveops.constructor_nallargs
 	  (Global.env ())
 	  constr
       in
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 13ff19a46b..7b758da8e8 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -361,7 +361,7 @@ let rec pattern_to_term pt = DAst.with_val (function
 	mkGVar id
   | PatCstr(constr,patternl,_) ->
       let cst_narg =
-	Inductiveops.constructor_nallargs_env
+        Inductiveops.constructor_nallargs
 	  (Global.env ())
 	  constr
       in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index a5c19f3217..e582362e25 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -382,8 +382,8 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	let _ =
 	  List.map_i
 	    (fun i x ->
-	     let princ = Indrec.lookup_eliminator (ind_kn,i) (InProp) in
-	     let env = Global.env () in
+              let env = Global.env () in
+              let princ = Indrec.lookup_eliminator env (ind_kn,i) (InProp) in
 	     let evd = ref (Evd.from_env env) in
 	     let evd',uprinc = Evd.fresh_global env !evd princ in
              let _ = evd := evd' in 
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 75565c1a34..2d40ba6562 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -119,7 +119,7 @@ let app_poly_check env evars f args =
   (evars, cstrs), t
 
 let app_poly_nocheck env evars f args =
-  let evars, fc = f evars in 
+  let evars, fc = f evars in
     evars, mkApp (fc, args)
 
 let app_poly_sort b =
@@ -175,25 +175,29 @@ end) = struct
 
   let rewrite_relation_class = find_global relation_classes "RewriteRelation"
 
-  let proper_class = lazy (class_info (find_reference morphisms "Proper"))
-  let proper_proxy_class = lazy (class_info (find_reference morphisms "ProperProxy"))
-    
-  let proper_proj = lazy (mkConst (Option.get (pi3 (List.hd (Lazy.force proper_class).cl_projs))))
-    
-  let proper_type = 
-    let l = lazy (Lazy.force proper_class).cl_impl in
-      fun (evd,cstrs) -> 
-        let (evd, c) = Evarutil.new_global evd (Lazy.force l) in
-	  (evd, cstrs), c
-	
-  let proper_proxy_type = 
-    let l = lazy (Lazy.force proper_proxy_class).cl_impl in
-      fun (evd,cstrs) -> 
-        let (evd, c) = Evarutil.new_global evd (Lazy.force l) in
-	  (evd, cstrs), c
+  let proper_class =
+    let r = lazy (find_reference morphisms "Proper") in
+    fun env sigma -> class_info env sigma (Lazy.force r)
+
+  let proper_proxy_class =
+    let r = lazy (find_reference morphisms "ProperProxy") in
+    fun env sigma -> class_info env sigma (Lazy.force r)
+
+  let proper_proj env sigma =
+    mkConst (Option.get (pi3 (List.hd (proper_class env sigma).cl_projs)))
+
+  let proper_type env (sigma,cstrs) =
+    let l = (proper_class env sigma).cl_impl in
+    let (sigma, c) = Evarutil.new_global sigma l in
+    (sigma, cstrs), c
+
+  let proper_proxy_type env (sigma,cstrs) =
+    let l = (proper_proxy_class env sigma).cl_impl in
+    let (sigma, c) = Evarutil.new_global sigma l in
+    (sigma, cstrs), c
 
   let proper_proof env evars carrier relation x =
-    let evars, goal = app_poly env evars proper_proxy_type [| carrier ; relation; x |] in
+    let evars, goal = app_poly env evars (proper_proxy_type env) [| carrier ; relation; x |] in
       new_cstr_evar evars env goal
 
   let get_reflexive_proof env = find_class_proof reflexive_type reflexive_proof env
@@ -800,7 +804,7 @@ let resolve_morphism env avoid oldt m ?(fnewt=fun x -> x) args args' (b,cstr) ev
     in
       (* Actual signature found *)
     let cl_args = [| appmtype' ; signature ; appm |] in
-    let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type else TypeGlobal.proper_type)
+    let evars, app = app_poly_sort b env evars (if b then PropGlobal.proper_type env else TypeGlobal.proper_type env)
       cl_args in
     let env' = 
       let dosub, appsub = 
@@ -1310,8 +1314,8 @@ module Strategies =
 	in
 	let evars, proof =
 	  let proxy = 
-	    if prop then PropGlobal.proper_proxy_type 
-	    else TypeGlobal.proper_proxy_type
+            if prop then PropGlobal.proper_proxy_type env
+            else TypeGlobal.proper_proxy_type env
 	  in
 	  let evars, mty = app_poly_sort prop env evars proxy [| ty ; rel; t |] in
 	    new_cstr_evar evars env mty
@@ -1854,12 +1858,12 @@ let declare_relation ~pstate atts ?(binders=[]) a aeq n refl symm trans =
 
 let cHole = CAst.make @@ CHole (None, Namegen.IntroAnonymous, None)
 
-let proper_projection sigma r ty =
+let proper_projection env sigma r ty =
   let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
   let ctx, inst = decompose_prod_assum sigma ty in
   let mor, args = destApp sigma inst in
   let instarg = mkApp (r, rel_vect 0 (List.length ctx)) in
-  let app = mkApp (Lazy.force PropGlobal.proper_proj,
+  let app = mkApp (PropGlobal.proper_proj env sigma,
 		  Array.append args [| instarg |]) in
     it_mkLambda_or_LetIn app ctx
 
@@ -1869,7 +1873,7 @@ let declare_projection n instance_id r =
   let sigma = Evd.from_env env in
   let sigma,c = Evd.fresh_global env sigma r in
   let ty = Retyping.get_type_of env sigma c in
-  let term = proper_projection sigma c ty in
+  let term = proper_projection env sigma c ty in
   let sigma, typ = Typing.type_of env sigma term in
   let ctx, typ = decompose_prod_assum sigma typ in
   let typ =
@@ -1924,7 +1928,7 @@ let build_morphism_signature env sigma m =
 	rel)
     cstrs
   in
-  let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in
+  let morph = e_app_poly env evd (PropGlobal.proper_type env) [| t; sig_; m |] in
   let evd = solve_constraints env !evd in
   let evd = Evd.minimize_universes evd in
   let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
@@ -1938,9 +1942,9 @@ let default_morphism sign m =
   let evars, _, sign, cstrs =
     PropGlobal.build_signature (sigma, Evar.Set.empty) env t (fst sign) (snd sign)
   in
-  let evars, morph = app_poly_check env evars PropGlobal.proper_type [| t; sign; m |] in
+  let evars, morph = app_poly_check env evars (PropGlobal.proper_type env) [| t; sign; m |] in
   let evars, mor = resolve_one_typeclass env (goalevars evars) morph in
-    mor, proper_projection sigma mor morph
+    mor, proper_projection env sigma mor morph
 
 let warn_add_setoid_deprecated =
   CWarnings.create ~name:"add-setoid" ~category:"deprecated" (fun () ->
@@ -1984,8 +1988,8 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
              (None,(instance,uctx),None),
            Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
-      add_instance (Typeclasses.new_instance
-                      (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info atts.global (ConstRef cst));
+      add_instance (Classes.mk_instance
+                      (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (ConstRef cst));
       declare_projection n instance_id (ConstRef cst);
       pstate
     else
@@ -1995,8 +1999,8 @@ let add_morphism_infer ~pstate atts m n : Proof_global.t option =
       let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
       let hook _ _ _ = function
         | Globnames.ConstRef cst ->
-          add_instance (Typeclasses.new_instance
-                          (Lazy.force PropGlobal.proper_class) Hints.empty_hint_info
+          add_instance (Classes.mk_instance
+                          (PropGlobal.proper_class env evd) Hints.empty_hint_info
                           atts.global (ConstRef cst));
           declare_projection n instance_id (ConstRef cst)
         | _ -> assert false
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index caaa547a07..e617f3d45e 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -30,7 +30,7 @@ let subst_quantified_hypothesis _ x = x
 let subst_declared_or_quantified_hypothesis _ x = x
 
 let subst_glob_constr_and_expr subst (c, e) =
-  (Detyping.subst_glob_constr subst c, e)
+  (Detyping.subst_glob_constr (Global.env()) subst c, e)
 
 let subst_glob_constr = subst_glob_constr_and_expr (* shortening *)
 
@@ -99,7 +99,9 @@ let subst_evaluable subst =
 let subst_constr_with_occurrences subst (l,c) = (l,subst_glob_constr subst c)
 
 let subst_glob_constr_or_pattern subst (bvars,c,p) =
-  (bvars,subst_glob_constr subst c,subst_pattern subst p)
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  (bvars,subst_glob_constr subst c,subst_pattern env sigma subst p)
 
 let subst_redexp subst =
   Redops.map_red_expr_gen
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 4c65445b89..d1951cc18d 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -98,16 +98,18 @@ let split = Tactics.split_with_bindings false [Tactypes.NoBindings]
 (** Test *)
 
 let is_empty _ ist =
+  Proofview.tclENV >>= fun genv ->
   Proofview.tclEVARMAP >>= fun sigma ->
-  if is_empty_type sigma (assoc_var "X1" ist) then idtac else fail
+  if is_empty_type genv sigma (assoc_var "X1" ist) then idtac else fail
 
 (* Strictly speaking, this exceeds the propositional fragment as it
    matches also equality types (and solves them if a reflexivity) *)
 let is_unit_or_eq _ ist =
+  Proofview.tclENV >>= fun genv ->
   Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let test = if flags.strict_unit then is_unit_type else is_unit_or_eq_type in
-  if test sigma (assoc_var "X1" ist) then idtac else fail
+  if test genv sigma (assoc_var "X1" ist) then idtac else fail
 
 let bugged_is_binary sigma t =
   isApp sigma t &&
@@ -121,23 +123,25 @@ let bugged_is_binary sigma t =
 (** Dealing with conjunction *)
 
 let is_conj _ ist =
+  Proofview.tclENV >>= fun genv ->
   Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let ind = assoc_var "X1" ist in
     if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma ind) &&
-       is_conjunction sigma
+       is_conjunction genv sigma
          ~strict:flags.strict_in_hyp_and_ccl
          ~onlybinary:flags.binary_mode ind
     then idtac
     else fail
 
 let flatten_contravariant_conj _ ist =
+  Proofview.tclENV >>= fun genv ->
   Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let typ = assoc_var "X1" ist in
   let c = assoc_var "X2" ist in
   let hyp = assoc_var "id" ist in
-  match match_with_conjunction sigma
+  match match_with_conjunction genv sigma
           ~strict:flags.strict_in_contravariant_hyp
           ~onlybinary:flags.binary_mode typ
   with
@@ -151,23 +155,25 @@ let flatten_contravariant_conj _ ist =
 (** Dealing with disjunction *)
 
 let is_disj _ ist =
+  Proofview.tclENV >>= fun genv ->
   Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let t = assoc_var "X1" ist in
   if (not flags.binary_mode_bugged_detection || bugged_is_binary sigma t) &&
-     is_disjunction sigma
+     is_disjunction genv sigma
        ~strict:flags.strict_in_hyp_and_ccl
        ~onlybinary:flags.binary_mode t
   then idtac
   else fail
 
 let flatten_contravariant_disj _ ist =
+  Proofview.tclENV >>= fun genv ->
   Proofview.tclEVARMAP >>= fun sigma ->
   let flags = assoc_flags ist in
   let typ = assoc_var "X1" ist in
   let c = assoc_var "X2" ist in
   let hyp = assoc_var "id" ist in
-  match match_with_disjunction sigma
+  match match_with_disjunction genv sigma
           ~strict:flags.strict_in_contravariant_hyp
           ~onlybinary:flags.binary_mode
           typ with
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml
index 350bb9019e..675e4d2457 100644
--- a/plugins/ssr/ssrelim.ml
+++ b/plugins/ssr/ssrelim.ml
@@ -194,7 +194,7 @@ let ssrelim ?(is_case=false) deps what ?elim eqid elim_intro_tac =
       let sort = Tacticals.elimination_sort_of_goal gl in
       let gl, elim =
         if not is_case then
-          let t,gl= pf_fresh_global (Indrec.lookup_eliminator (kn,i) sort) gl in
+          let t,gl= pf_fresh_global (Indrec.lookup_eliminator env (kn,i) sort) gl in
           gl, t
         else
           Tacmach.pf_eapply (fun env sigma () ->
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 5abbc214de..4433f2fce7 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -340,7 +340,7 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl =
   let elim, gl = 
     let ((kn, i) as ind, _), unfolded_c_ty = pf_reduce_to_quantified_ind gl c_ty in
     let sort = elimination_sort_of_goal gl in
-    let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in
+    let elim, gl = pf_fresh_global (Indrec.lookup_eliminator env ind sort) gl in
     if dir = R2L then elim, gl else (* taken from Coq's rewrite *)
     let elim, _ = destConst elim in
     let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical elim)) in
@@ -504,9 +504,9 @@ let rwprocess_rule dir rule gl =
          let sigma, rs2 = loop d sigma s a.(1) rs 0 in
          let s, sigma = sr sigma 1 in
          loop d sigma s a.(0) rs2 0
-      | App (r_eq, a) when Hipattern.match_with_equality_type sigma t != None ->
+      | App (r_eq, a) when Hipattern.match_with_equality_type env sigma t != None ->
         let (ind, u) = EConstr.destInd sigma r_eq and rhs = Array.last a in
-        let np = Inductiveops.inductive_nparamdecls ind in
+        let np = Inductiveops.inductive_nparamdecls env ind in
         let indu = (ind, EConstr.EInstance.kind sigma u) in
         let ind_ct = Inductiveops.type_of_constructors env indu in
         let lhs0 = last_arg sigma (EConstr.of_constr (strip_prod_assum ind_ct.(0))) in
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 537fd7d7b4..075ebf006a 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -43,7 +43,7 @@ module AdaptorDb = struct
       term_view_adaptor_db := AdaptorMap.add k (t :: lk) !term_view_adaptor_db
 
   let subst_adaptor ( subst, (k, t as a)) =
-    let t' = Detyping.subst_glob_constr subst t in
+    let t' = Detyping.subst_glob_constr (Global.env()) subst t in
     if t' == t then a else k, t'
 
   let in_db =
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
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 8bf86e9ef6..9541ea5882 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -952,5 +952,6 @@ let print_all_instances () =
 
 let print_instances r =
   let env = Global.env () in
-  let inst = instances r in
+  let sigma = Evd.from_env env in
+  let inst = instances env sigma r in
     prlist_with_sep fnl (pr_instance env) inst
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index a28f4597cf..c1ac7d201a 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -362,7 +362,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm
     try
       match hdc with
       | Some (hd,_) when only_classes ->
-         let cl = Typeclasses.class_info hd in
+         let cl = Typeclasses.class_info env sigma hd in
          if cl.cl_strict then
            Evarutil.undefined_evars_of_term sigma concl
          else Evar.Set.empty
@@ -1052,7 +1052,7 @@ let error_unresolvable env comp evd =
   | Some s -> Evar.Set.mem ev s
   in
   let fold ev evi (found, accu) =
-    let ev_class = class_of_constr evd evi.evar_concl in
+    let ev_class = class_of_constr env evd evi.evar_concl in
     if not (Option.is_empty ev_class) && is_part ev then
       (* focus on one instance if only one was searched for *)
       if not found then (true, Some ev)
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 3ff2e3852d..d9d3764b2a 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -67,17 +67,17 @@ let contradiction_context =
           let id = NamedDecl.get_id d in
           let typ = nf_evar sigma (NamedDecl.get_type d) in
 	  let typ = whd_all env sigma typ in
-	  if is_empty_type sigma typ then
+          if is_empty_type env sigma typ then
 	    simplest_elim (mkVar id)
 	  else match EConstr.kind sigma typ with
-          | Prod (na,t,u) when is_empty_type sigma u ->
-             let is_unit_or_eq = match_with_unit_or_eq_type sigma t in
+          | Prod (na,t,u) when is_empty_type env sigma u ->
+             let is_unit_or_eq = match_with_unit_or_eq_type env sigma t in
              Tacticals.New.tclORELSE
                (match is_unit_or_eq with
                | Some _ ->
                    let hd,args = decompose_app sigma t in
                    let (ind,_ as indu) = destInd sigma hd in
-                   let nparams = Inductiveops.inductive_nparams_env env ind in
+                   let nparams = Inductiveops.inductive_nparams env ind in
                    let params = Util.List.firstn nparams args in
                    let p = applist ((mkConstructUi (indu,1)), params) in
                    (* Checking on the fly that it type-checks *)
@@ -103,7 +103,7 @@ let contradiction_context =
 let is_negation_of env sigma typ t =
   match EConstr.kind sigma (whd_all env sigma t) with
     | Prod (na,t,u) ->
-      is_empty_type sigma u && is_conv_leq env sigma typ t
+      is_empty_type env sigma u && is_conv_leq env sigma typ t
     | _ -> false
 
 let contradiction_term (c,lbind as cl) =
@@ -113,7 +113,7 @@ let contradiction_term (c,lbind as cl) =
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let typ = type_of c in
     let _, ccl = splay_prod env sigma typ in
-    if is_empty_type sigma ccl then
+    if is_empty_type env sigma ccl then
       Tacticals.New.tclTHEN
         (elim false None cl None)
         (Tacticals.New.tclTRY assumption)
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 003b069b6e..71ea0098a3 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -81,12 +81,13 @@ let up_to_delta = ref false (* true *)
 let general_decompose recognizer c =
   Proofview.Goal.enter begin fun gl ->
   let type_of = pf_unsafe_type_of gl in
+  let env = pf_env gl in
   let sigma = project gl in
   let typc = type_of c in
   tclTHENS (cut typc)
     [ tclTHEN (intro_using tmphyp_name)
          (onLastHypId
-	    (ifOnHyp (recognizer sigma) (general_decompose_aux (recognizer sigma))
+            (ifOnHyp (recognizer env sigma) (general_decompose_aux (recognizer env sigma))
 	      (fun id -> clear [id])));
        exact_no_check c ]
   end
@@ -105,17 +106,17 @@ let head_in indl t gl =
 let decompose_these c l =
   Proofview.Goal.enter begin fun gl ->
   let indl = List.map (fun x -> x, Univ.Instance.empty) l in
-  general_decompose (fun sigma (_,t) -> head_in indl t gl) c
+  general_decompose (fun env sigma (_,t) -> head_in indl t gl) c
   end
 
 let decompose_and c =
   general_decompose
-    (fun sigma (_,t) -> is_record sigma t)
+    (fun env sigma (_,t) -> is_record env sigma t)
     c
 
 let decompose_or c =
   general_decompose
-    (fun sigma (_,t) -> is_disjunction sigma t)
+    (fun env sigma (_,t) -> is_disjunction env sigma t)
     c
 
 let h_decompose l c = decompose_these c l
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 412fbbfd1b..3d760f1c3d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -356,7 +356,7 @@ let find_elim hdcncl lft2rgt dep cls ot =
       match EConstr.kind sigma hdcncl with 
       | Ind (ind_sp,u) -> 
 	let pr1 = 
-	  lookup_eliminator ind_sp (elimination_sort_of_clause cls gl) 
+          lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl)
 	in
         begin match lft2rgt, cls with
         | Some true, None
@@ -446,7 +446,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
       let env = Proofview.Goal.env gl in
     let ctype = get_type_of env sigma c in
     let rels, t = decompose_prod_assum sigma (whd_betaiotazeta sigma ctype) in
-      match match_with_equality_type sigma t with
+      match match_with_equality_type env sigma t with
       | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *)
 	  let lft2rgt = adjust_rewriting_direction args lft2rgt in
           leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels)
@@ -462,7 +462,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
                   Proofview.tclEVARMAP >>= fun sigma ->
 	          let env' = push_rel_context rels env in
 	          let rels',t' = splay_prod_assum env' sigma t in (* Search for underlying eq *)
-	          match match_with_equality_type sigma t' with
+                  match match_with_equality_type env sigma t' with
 	            | Some (hdcncl,args) ->
 		  let lft2rgt = adjust_rewriting_direction args lft2rgt in
 		  leibniz_rewrite_ebindings_clause cls lft2rgt tac c
@@ -743,7 +743,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
     let hd2,args2 = whd_all_stack env sigma t2 in
     match (EConstr.kind sigma hd1, EConstr.kind sigma hd2) with
       | Construct ((ind1,i1 as sp1),u1), Construct (sp2,_)
-          when Int.equal (List.length args1) (constructor_nallargs_env env sp1)
+          when Int.equal (List.length args1) (constructor_nallargs env sp1)
             ->
 	  let sorts' =
             Sorts.List.intersect sorts (allowed_sorts env (fst sp1))
@@ -751,7 +751,7 @@ let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
           (* both sides are fully applied constructors, so either we descend,
              or we can discriminate here. *)
 	  if eq_constructor sp1 sp2 then
-	    let nparams = inductive_nparams_env env ind1 in
+            let nparams = inductive_nparams env ind1 in
 	    let params1,rargs1 = List.chop nparams args1 in
 	    let _,rargs2 = List.chop nparams args2 in
             let (mib,mip) = lookup_mind_specif env ind1 in
@@ -966,9 +966,10 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function
 
 let gen_absurdity id =
   Proofview.Goal.enter begin fun gl ->
+  let env = pf_env gl in
   let sigma = project gl in
   let hyp_typ = pf_get_hyp_typ id gl in
-  if is_empty_type sigma hyp_typ
+  if is_empty_type env sigma hyp_typ
   then
     simplest_elim (mkVar id)
   else
@@ -1066,7 +1067,7 @@ let onNegatedEquality with_evars tac =
     let ccl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
     match EConstr.kind sigma (hnf_constr env sigma ccl) with
-    | Prod (_,t,u) when is_empty_type sigma u ->
+    | Prod (_,t,u) when is_empty_type env sigma u ->
         tclTHEN introf
           (onLastHypId (fun id ->
             onEquality with_evars tac (mkVar id,NoBindings)))
diff --git a/tactics/hints.ml b/tactics/hints.ml
index f49b1660b8..11a8816159 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1064,7 +1064,9 @@ let subst_autohint (subst, obj) =
   in
   let subst_hint (k,data as hint) =
     let k' = Option.Smart.map subst_key k in
-    let pat' = Option.Smart.map (subst_pattern subst) data.pat in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    let pat' = Option.Smart.map (subst_pattern env sigma subst) data.pat in
     let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
     let code' = match data.code.obj with
       | Res_pf (c,t,ctx) ->
@@ -1353,7 +1355,7 @@ let interp_hints poly =
         let ind = global_inductive_with_alias qid in
 	let mib,_ = Global.lookup_inductive ind in
         Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind";
-          List.init (nconstructors ind) 
+          List.init (nconstructors env ind)
 	    (fun i -> let c = (ind,i+1) in
 		      let gr = ConstructRef c in
 			empty_hint_info, 
@@ -1389,7 +1391,7 @@ let expand_constructor_hints env sigma lems =
   List.map_append (fun (evd,lem) ->
     match EConstr.kind sigma lem with
     | Ind (ind,u) ->
-	List.init (nconstructors ind) 
+        List.init (nconstructors env ind)
 		  (fun i ->
 		   let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd)
 						  (Evd.universe_context_set sigma) in
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 08131f6309..e1dad9ad20 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -34,44 +34,42 @@ module RelDecl = Context.Rel.Declaration
 
   -- Eduardo (6/8/97). *)
 
-type 'a matching_function = Evd.evar_map -> EConstr.constr -> 'a option
+type 'a matching_function = Environ.env -> Evd.evar_map -> EConstr.constr -> 'a option
 
-type testing_function  = Evd.evar_map -> EConstr.constr -> bool
+type testing_function  = Environ.env -> Evd.evar_map -> EConstr.constr -> bool
 
 let mkmeta n = Nameops.make_ident "X" (Some n)
 let meta1 = mkmeta 1
 let meta2 = mkmeta 2
 
-let op2bool = function Some _ -> true | None -> false
-
-let match_with_non_recursive_type sigma t =
+let match_with_non_recursive_type env sigma t =
   match EConstr.kind sigma t with
     | App _ ->
         let (hdapp,args) = decompose_app sigma t in
         (match EConstr.kind sigma hdapp with
            | Ind (ind,u) ->
-               if (Global.lookup_mind (fst ind)).mind_finite == CoFinite then
+               if (Environ.lookup_mind (fst ind) env).mind_finite == CoFinite then
 		 Some (hdapp,args)
 	       else
 		 None
            | _ -> None)
     | _ -> None
 
-let is_non_recursive_type sigma t = op2bool (match_with_non_recursive_type sigma t)
+let is_non_recursive_type env sigma t = Option.has_some (match_with_non_recursive_type env sigma t)
 
 (* Test dependencies *)
 
 (* NB: we consider also the let-in case in the following function,
    since they may appear in types of inductive constructors (see #2629) *)
 
-let rec has_nodep_prod_after n sigma c =
+let rec has_nodep_prod_after n env sigma c =
   match EConstr.kind sigma c with
     | Prod (_,_,b) | LetIn (_,_,_,b) ->
 	( n>0 || Vars.noccurn sigma 1 b)
-	&& (has_nodep_prod_after (n-1) sigma b)
+        && (has_nodep_prod_after (n-1) env sigma b)
     | _            -> true
 
-let has_nodep_prod sigma c = has_nodep_prod_after 0 sigma c
+let has_nodep_prod env sigma c = has_nodep_prod_after 0 env sigma c
 
 (* A general conjunctive type is a non-recursive with-no-indices inductive
    type with only one constructor and no dependencies between argument;
@@ -96,11 +94,11 @@ let rec whd_beta_prod sigma c = match EConstr.kind sigma c with
   | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod sigma c)
   | _ -> c
 
-let match_with_one_constructor sigma style onlybinary allow_rec t =
+let match_with_one_constructor env sigma style onlybinary allow_rec t =
   let (hdapp,args) = decompose_app sigma t in
   let res = match EConstr.kind sigma hdapp with
   | Ind ind ->
-      let (mib,mip) = Global.lookup_inductive (fst ind) in
+      let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
       if Int.equal (Array.length mip.mind_consnames) 1
 	&& (allow_rec || not (mis_is_recursive (fst ind,mib,mip)))
         && (Int.equal mip.mind_nrealargs 0)
@@ -125,7 +123,7 @@ let match_with_one_constructor sigma style onlybinary allow_rec t =
           let ctyp = whd_beta_prod sigma
             (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt) cty args) in
 	  let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in
-	  if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then
+          if not (is_lax_conjunction style) || has_nodep_prod env sigma ctyp then
 	    (* Record or non strict conjunction *)
 	    Some (hdapp,List.rev cargs)
 	  else
@@ -138,20 +136,20 @@ let match_with_one_constructor sigma style onlybinary allow_rec t =
   | Some (hdapp, [_; _]) -> res
   | _ -> None
 
-let match_with_conjunction ?(strict=false) ?(onlybinary=false) sigma t =
-  match_with_one_constructor sigma (Some strict) onlybinary false t
+let match_with_conjunction ?(strict=false) ?(onlybinary=false) env sigma t =
+  match_with_one_constructor env sigma (Some strict) onlybinary false t
 
-let match_with_record sigma t =
-  match_with_one_constructor sigma None false false t
+let match_with_record env sigma t =
+  match_with_one_constructor env sigma None false false t
 
-let is_conjunction ?(strict=false) ?(onlybinary=false) sigma t =
-  op2bool (match_with_conjunction sigma ~strict ~onlybinary t)
+let is_conjunction ?(strict=false) ?(onlybinary=false) env sigma t =
+  Option.has_some (match_with_conjunction env sigma ~strict ~onlybinary t)
 
-let is_record sigma t =
-  op2bool (match_with_record sigma t)
+let is_record env sigma t =
+  Option.has_some (match_with_record env sigma t)
 
-let match_with_tuple sigma t =
-  let t = match_with_one_constructor sigma None false true t in
+let match_with_tuple env sigma t =
+  let t = match_with_one_constructor env sigma None false true t in
   Option.map (fun (hd,l) ->
     let ind = destInd sigma hd in
     let ind = on_snd (fun u -> EInstance.kind sigma u) ind in
@@ -159,8 +157,8 @@ let match_with_tuple sigma t =
     let isrec = mis_is_recursive (fst ind,mib,mip) in
     (hd,l,isrec)) t
 
-let is_tuple sigma t =
-  op2bool (match_with_tuple sigma t)
+let is_tuple env sigma t =
+  Option.has_some (match_with_tuple env sigma t)
 
 (* A general disjunction type is a non-recursive with-no-indices inductive
    type with of which all constructors have a single argument;
@@ -175,11 +173,11 @@ let test_strict_disjunction (mib, mip) =
   in
   Array.for_all_i check 0 mip.mind_nf_lc
 
-let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
+let match_with_disjunction ?(strict=false) ?(onlybinary=false) env sigma t =
   let (hdapp,args) = decompose_app sigma t in
   let res = match EConstr.kind sigma hdapp with
   | Ind (ind,u)  ->
-      let car = constructors_nrealargs ind in
+      let car = constructors_nrealargs env ind in
       let (mib,mip) = Global.lookup_inductive ind in
       if Array.for_all (fun ar -> Int.equal ar 1) car
       && not (mis_is_recursive (ind,mib,mip))
@@ -205,31 +203,31 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
   | Some (hdapp,[_; _]) -> res
   | _ -> None
 
-let is_disjunction ?(strict=false) ?(onlybinary=false) sigma t =
-  op2bool (match_with_disjunction ~strict ~onlybinary sigma t)
+let is_disjunction ?(strict=false) ?(onlybinary=false) env sigma t =
+  Option.has_some (match_with_disjunction ~strict ~onlybinary env sigma t)
 
 (* An empty type is an inductive type, possible with indices, that has no
    constructors *)
 
-let match_with_empty_type sigma t =
+let match_with_empty_type env sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
     | Ind (ind, _) ->
-        let (mib,mip) = Global.lookup_inductive ind in
+        let (mib,mip) = Inductive.lookup_mind_specif env ind in
         let nconstr = Array.length mip.mind_consnames in
 	if Int.equal nconstr 0 then Some hdapp else None
     | _ ->  None
 
-let is_empty_type sigma t = op2bool (match_with_empty_type sigma t)
+let is_empty_type env sigma t = Option.has_some (match_with_empty_type env sigma t)
 
 (* This filters inductive types with one constructor with no arguments;
    Parameters and indices are allowed *)
 
-let match_with_unit_or_eq_type sigma t =
+let match_with_unit_or_eq_type env sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
     | Ind (ind , _) ->
-        let (mib,mip) = Global.lookup_inductive ind in
+        let (mib,mip) = Inductive.lookup_mind_specif env ind in
         let nconstr = Array.length mip.mind_consnames in
         if Int.equal nconstr 1 && Int.equal mip.mind_consnrealargs.(0) 0 then
 	  Some hdapp
@@ -237,14 +235,14 @@ let match_with_unit_or_eq_type sigma t =
 	  None
     | _ -> None
 
-let is_unit_or_eq_type sigma t = op2bool (match_with_unit_or_eq_type sigma t)
+let is_unit_or_eq_type env sigma t = Option.has_some (match_with_unit_or_eq_type env sigma t)
 
 (* A unit type is an inductive type with no indices but possibly
    (useless) parameters, and that has no arguments in its unique
    constructor *)
 
-let is_unit_type sigma t =
-  match match_with_conjunction sigma t with
+let is_unit_type env sigma t =
+  match match_with_conjunction env sigma t with
   | Some (_,[]) -> true
   | _ -> false
 
@@ -331,15 +329,16 @@ let match_with_equation env sigma t =
 let is_inductive_equality ind =
   let (mib,mip) = Global.lookup_inductive ind in
   let nconstr = Array.length mip.mind_consnames in
-  Int.equal nconstr 1 && Int.equal (constructor_nrealargs (ind,1)) 0
+  let env = Global.env () in
+  Int.equal nconstr 1 && Int.equal (constructor_nrealargs env (ind,1)) 0
 
-let match_with_equality_type sigma t =
+let match_with_equality_type env sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
   | Ind (ind,_) when is_inductive_equality ind -> Some (hdapp,args)
   | _ -> None
 
-let is_equality_type sigma t = op2bool (match_with_equality_type sigma t)
+let is_equality_type env sigma t = Option.has_some (match_with_equality_type env sigma t)
 
 (* Arrows/Implication/Negation *)
 
@@ -353,39 +352,39 @@ let match_arrow_pattern env sigma t =
       assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind)
     | _ -> anomaly (Pp.str "Incorrect pattern matching.")
 
-let match_with_imp_term sigma c =
+let match_with_imp_term env sigma c =
   match EConstr.kind sigma c with
     | Prod (_,a,b) when Vars.noccurn sigma 1 b -> Some (a,b)
     | _              -> None
 
-let is_imp_term sigma c = op2bool (match_with_imp_term sigma c)
+let is_imp_term env sigma c = Option.has_some (match_with_imp_term env sigma c)
 
 let match_with_nottype env sigma t =
   try
     let (arg,mind) = match_arrow_pattern env sigma t in
-    if is_empty_type sigma mind then Some (mind,arg) else None
+    if is_empty_type env sigma mind then Some (mind,arg) else None
   with PatternMatchingFailure -> None
 
-let is_nottype env sigma t = op2bool (match_with_nottype env sigma t)
+let is_nottype env sigma t = Option.has_some (match_with_nottype env sigma t)
 
 (* Forall *)
 
-let match_with_forall_term sigma c=
+let match_with_forall_term env sigma c =
   match EConstr.kind sigma c with
     | Prod (nam,a,b) -> Some (nam,a,b)
     | _            -> None
 
-let is_forall_term sigma c = op2bool (match_with_forall_term sigma c)
+let is_forall_term env sigma c = Option.has_some (match_with_forall_term env sigma c)
 
-let match_with_nodep_ind sigma t =
+let match_with_nodep_ind env sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
   | Ind (ind, _)  ->
-     let (mib,mip) = Global.lookup_inductive ind in
+     let (mib,mip) = Inductive.lookup_mind_specif env ind in
      if Array.length (mib.mind_packets)>1 then None else
        let nodep_constr (ctx, cty) =
         let c = EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx) in
-         has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) sigma c in
+         has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt) env sigma c in
        if Array.for_all nodep_constr mip.mind_nf_lc then
          let params=
            if Int.equal mip.mind_nrealargs 0 then args else
@@ -395,9 +394,9 @@ let match_with_nodep_ind sigma t =
          None
   | _ -> None
 
-let is_nodep_ind sigma t = op2bool (match_with_nodep_ind sigma t)
+let is_nodep_ind env sigma t = Option.has_some (match_with_nodep_ind env sigma t)
 
-let match_with_sigma_type sigma t =
+let match_with_sigma_type env sigma t =
   let (hdapp,args) = decompose_app sigma t in
   match EConstr.kind sigma hdapp with
   | Ind (ind, _) ->
@@ -405,7 +404,7 @@ let match_with_sigma_type sigma t =
      if Int.equal (Array.length (mib.mind_packets)) 1
         && (Int.equal mip.mind_nrealargs 0)
         && (Int.equal (Array.length mip.mind_consnames)1)
-        && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) sigma
+        && has_nodep_prod_after (Context.Rel.length mib.mind_params_ctxt + 1) env sigma
              (let (ctx, cty) = mip.mind_nf_lc.(0) in EConstr.of_constr (Term.it_mkProd_or_LetIn cty ctx))
      then
        (*allowing only 1 existential*)
@@ -414,7 +413,7 @@ let match_with_sigma_type sigma t =
        None
   | _ -> None
 
-let is_sigma_type sigma t = op2bool (match_with_sigma_type sigma t)
+let is_sigma_type env sigma t = Option.has_some (match_with_sigma_type env sigma t)
 
 (***** Destructing patterns bound to some theory *)
 
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 741f6713e3..b8c3ddb0f0 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -43,8 +43,8 @@ open Coqlib
    also work on ad-hoc disjunctions introduced by the user.
    (Eduardo, 6/8/97). *)
 
-type 'a matching_function = evar_map -> constr -> 'a option
-type testing_function = evar_map -> constr -> bool
+type 'a matching_function = Environ.env -> evar_map -> constr -> 'a option
+type testing_function = Environ.env -> evar_map -> constr -> bool
 
 val match_with_non_recursive_type : (constr * constr list) matching_function
 val is_non_recursive_type         : testing_function
@@ -83,8 +83,8 @@ val is_inductive_equality  : inductive -> bool
 val match_with_equality_type : (constr * constr list) matching_function
 val is_equality_type       : testing_function
 
-val match_with_nottype     : Environ.env -> (constr * constr) matching_function
-val is_nottype             : Environ.env -> testing_function
+val match_with_nottype     : (constr * constr) matching_function
+val is_nottype             : testing_function
 
 val match_with_forall_term    : (Name.t Context.binder_annot * constr * constr) matching_function
 val is_forall_term            : testing_function
diff --git a/tactics/redexpr.ml b/tactics/redexpr.ml
index aabfae444e..447b908a1d 100644
--- a/tactics/redexpr.ml
+++ b/tactics/redexpr.ml
@@ -259,10 +259,12 @@ let subst_mps subst c =
   EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
 
 let subst_red_expr subs =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
   Redops.map_red_expr_gen
     (subst_mps subs)
     (Mod_subst.subst_evaluable_reference subs)
-    (Patternops.subst_pattern subs)
+    (Patternops.subst_pattern env sigma subs)
 
 let inReduction : bool * string * red_expr -> obj =
   declare_object
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index ec8d4d0e14..dcd63fe760 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -704,7 +704,8 @@ module New = struct
   (* computing the case/elim combinators *)
 
   let gl_make_elim ind = begin fun gl ->
-    let gr = Indrec.lookup_eliminator (fst ind) (elimination_sort_of_goal gl) in
+    let env = Proofview.Goal.env gl in
+    let gr = Indrec.lookup_eliminator env (fst ind) (elimination_sort_of_goal gl) in
     let (sigma, c) = pf_apply Evd.fresh_global gl gr in
     (sigma, c)
   end
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 206f35c8ba..066b9c7794 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1432,7 +1432,7 @@ let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
   Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
   (general_elim with_evars clear_flag (c,lbindc)
    {elimindex = None; elimbody = (elim,NoBindings);
-    elimrename = Some (false, constructors_nrealdecls (fst mind))})
+    elimrename = Some (false, constructors_nrealdecls env (fst mind))})
   end
 
 let general_case_analysis with_evars clear_flag (c,lbindc as cx) =
@@ -1455,7 +1455,8 @@ exception IsNonrec
 let is_nonrec mind = (Global.lookup_mind (fst mind)).mind_finite == Declarations.BiFinite
 
 let find_ind_eliminator ind s gl =
-  let gr = lookup_eliminator ind s in
+  let env = Proofview.Goal.env gl in
+  let gr = lookup_eliminator env ind s in
   Tacmach.New.pf_apply Evd.fresh_global gl gr
 
 let find_eliminator c gl =
@@ -1463,7 +1464,7 @@ let find_eliminator c gl =
   if is_nonrec ind then raise IsNonrec;
   let evd, c = find_ind_eliminator ind (Tacticals.New.elimination_sort_of_goal gl) gl in
     evd, {elimindex = None; elimbody = (c,NoBindings);
-          elimrename = Some (true, constructors_nrealdecls ind)}
+          elimrename = Some (true, constructors_nrealdecls (Global.env()) ind)}
 
 let default_elim with_evars clear_flag (c,_ as cx) =
   Proofview.tclORELSE
@@ -1609,9 +1610,9 @@ let descend_in_conjunctions avoid tac (err, info) c =
     let t = Retyping.get_type_of env sigma c in
     let ((ind,u),t) = reduce_to_quantified_ind env sigma t in
     let sign,ccl = EConstr.decompose_prod_assum sigma t in
-    match match_with_tuple sigma ccl with
+    match match_with_tuple env sigma ccl with
     | Some (_,_,isrec) ->
-	let n = (constructors_nrealargs ind).(0) in
+        let n = (constructors_nrealargs env ind).(0) in
 	let sort = Tacticals.New.elimination_sort_of_goal gl in
 	let IndType (indf,_) = find_rectype env sigma ccl in
 	let (_,inst), params = dest_ind_family indf in
@@ -2299,7 +2300,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac =
     let type_of = Tacmach.New.pf_unsafe_type_of gl in
     let whd_all = Tacmach.New.pf_apply whd_all gl in
     let t = whd_all (type_of (mkVar id)) in
-    let eqtac, thin = match match_with_equality_type sigma t with
+    let eqtac, thin = match match_with_equality_type env sigma t with
     | Some (hdcncl,[_;lhs;rhs]) ->
         if l2r && isVar sigma lhs && not (occur_var env sigma (destVar sigma lhs) rhs) then
           let id' = destVar sigma lhs in
@@ -4128,7 +4129,7 @@ let guess_elim isrec dep s hyp0 gl =
   let sigma, elimc =
     if isrec && not (is_nonrec mind)
     then
-      let gr = lookup_eliminator mind s in
+      let gr = lookup_eliminator env mind s in
       Evd.fresh_global env sigma gr
     else
       let u = EInstance.kind sigma u in
@@ -4739,9 +4740,10 @@ let reflexivity_red allowred =
   (* PL: usual reflexivity don't perform any reduction when searching
      for an equality, but we may need to do some when called back from
      inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
+    let env = Tacmach.New.pf_env gl in
     let sigma = Tacmach.New.project gl in
     let concl = maybe_betadeltaiota_concl allowred gl in
-    match match_with_equality_type sigma concl with
+    match match_with_equality_type env sigma concl with
     | None -> Proofview.tclZERO NoEquationFound
     | Some _ -> one_constructor 1 NoBindings
   end
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/class.ml b/vernac/class.ml
index 0837beccee..f3a279eab1 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -23,6 +23,7 @@ open Classops
 open Declare
 open Globnames
 open Decl_kinds
+open Libobject
 
 let strength_min l = if List.mem `LOCAL l then `LOCAL else `GLOBAL
 
@@ -230,6 +231,58 @@ let check_source = function
 | Some (CL_FUN as s) -> raise (CoercionError (ForbiddenSourceClass s))
 | _ -> ()
 
+let cache_coercion (_,c) =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  Classops.declare_coercion env sigma c
+
+let open_coercion i o =
+  if Int.equal i 1 then
+    cache_coercion o
+
+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 = (fun (subst,c) -> subst_coercion subst c);
+    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)
+
 (*
 nom de la fonction coercion
 strength de f
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d61d324941..9f233a2551 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -22,8 +22,10 @@ open Constrintern
 open Constrexpr
 open Context.Rel.Declaration
 open Class_tactics
+open Libobject
 
 module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
 (*i*)
 
 open Decl_kinds
@@ -49,17 +51,224 @@ let classes_transparent_state () =
   with Not_found -> TransparentState.empty
 
 let () =
-  Hook.set Typeclasses.add_instance_hint_hook
-    (fun inst path local info poly ->
+  Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
+  Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state
+
+let add_instance_hint inst path local info poly =
      let inst' = match inst with IsConstr c -> Hints.IsConstr (EConstr.of_constr c, Univ.ContextSet.empty)
        | IsGlobal gr -> Hints.IsGlobRef gr
      in
      Flags.silently (fun () ->
        Hints.add_hints ~local [typeclasses_db]
 	  (Hints.HintsResolveEntry
-	     [info, poly, false, Hints.PathHints path, inst'])) ());
-  Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
-  Hook.set Typeclasses.classes_transparent_state_hook classes_transparent_state
+             [info, poly, false, Hints.PathHints path, inst'])) ()
+
+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 mk_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 }
+
+(*
+ * instances persistent object
+ *)
+let cache_instance (_, i) =
+  load_instance i
+
+let subst_instance (subst, inst) =
+  { inst with
+      is_class = fst (subst_global subst inst.is_class);
+      is_impl = fst (subst_global subst inst.is_impl) }
+
+let discharge_instance (_, inst) =
+  match inst.is_global with
+  | None -> None
+  | Some n ->
+    assert (not (isVarRef inst.is_impl));
+    Some
+    { 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 rebuild_instance inst =
+  add_instance true inst;
+  inst
+
+let classify_instance inst =
+  if is_local inst then Dispose
+  else Substitute inst
+
+let instance_input : 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 i);
+  add_instance true i
+
+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) env sigma info local glob =
+  let ty, _ = Typeops.type_of_global_in_context env glob in
+  let info = Option.default {hint_priority = None; hint_pattern = None} info in
+  match class_of_constr env sigma (EConstr.of_constr ty) with
+  | Some (rels, ((tc,_), args) as _cl) ->
+    assert (not (isVarRef glob) || local);
+    add_instance (mk_instance tc info (not local) glob)
+  | None -> if warn then warning_not_a_class (glob, ty)
+
+(*
+ * classes persistent object
+ *)
+
+let cache_class (_,c) = load_class c
+
+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 open CVars in
+  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 env = Global.env () in
+    let sigma = Evd.from_env env in
+    let grs' =
+      let newgrs = List.map (fun decl ->
+                             match decl |> RelDecl.get_type |> EConstr.of_constr |> class_of_constr env sigma 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 _ -> cache_class);
+      open_function = (fun _ -> cache_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)
+
+let add_class env sigma 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 env sigma (Some info) false (ConstRef b))
+      | _ -> ())
+    cl.cl_projs
 
 let intern_info {hint_priority;hint_pattern} =
   let env = Global.env() in
@@ -72,10 +281,12 @@ let existing_instance glob g info =
   let c = Nametab.global g in
   let info = Option.default Hints.empty_hint_info info in
   let info = intern_info info in
-  let instance, _ = Typeops.type_of_global_in_context (Global.env ()) c in
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
+  let instance, _ = Typeops.type_of_global_in_context env c in
   let _, r = Term.decompose_prod_assum instance in
-    match class_of_constr Evd.empty (EConstr.of_constr r) with
-      | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob c)
+    match class_of_constr env sigma (EConstr.of_constr r) with
+      | Some (_, ((tc,u), _)) -> add_instance (mk_instance tc info glob c)
       | None -> user_err ?loc:g.CAst.loc
                          ~hdr:"declare_instance"
                          (Pp.str "Constant does not build instances of a declared type class.")
@@ -111,7 +322,9 @@ let id_of_class cl =
 let instance_hook k info global imps ?hook cst =
   Impargs.maybe_declare_manual_implicits false cst imps;
   let info = intern_info info in
-  Typeclasses.declare_instance (Some info) (not global) cst;
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  declare_instance env sigma (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
 let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype =
@@ -154,7 +367,9 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po
       let cst = match gr with ConstRef kn -> kn | _ -> assert false in
       Impargs.declare_manual_implicits false gr imps;
       let pri = intern_info pri in
-      Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
+      let env = Global.env () in
+      let sigma = Evd.from_env env in
+      declare_instance env sigma (Some pri) (not global) (ConstRef cst)
     in
     let obls, constr, typ =
       match term with
@@ -360,96 +575,3 @@ let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl)
     interp_instance_context ~program_mode env ctx pl bk cl
   in
   do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst instid
-
-let named_of_rel_context l =
-  let open Vars in
-  let acc, ctx =
-    List.fold_right
-      (fun decl (subst, ctx) ->
-        let id = match RelDecl.get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
-	let d = match decl with
-          | LocalAssum (_,t) -> id, None, substl subst t
-          | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
-	  (mkVar id :: subst, d :: ctx))
-      l ([], [])
-  in ctx
-
-let context ~pstate poly l =
-  let env = Global.env() in
-  let sigma = Evd.from_env env in
-  let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
-  (* Note, we must use the normalized evar from now on! *)
-  let sigma = Evd.minimize_universes sigma in
-  let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in
-  let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
-  let ctx =
-    try named_of_rel_context fullctx
-    with e when CErrors.noncritical e ->
-      user_err Pp.(str "Anonymous variables not allowed in contexts.")
-  in
-  let univs =
-    match ctx with
-    | [] -> assert false
-    | [_] -> Evd.univ_entry ~poly sigma
-    | _::_::_ ->
-      if Lib.sections_are_opened ()
-      then
-        (* More than 1 variable in a section: we can't associate
-           universes to any specific variable so we declare them
-           separately. *)
-        begin
-          let uctx = Evd.universe_context_set sigma in
-          Declare.declare_universe_context poly uctx;
-          if poly then Polymorphic_entry ([||], Univ.UContext.empty)
-          else Monomorphic_entry Univ.ContextSet.empty
-        end
-      else if poly then
-        (* Multiple polymorphic axioms: they are all polymorphic the same way. *)
-        Evd.univ_entry ~poly sigma
-      else
-        (* Multiple monomorphic axioms: declare universes separately
-           to avoid redeclaring them. *)
-        begin
-          let uctx = Evd.universe_context_set sigma in
-          Declare.declare_universe_context poly uctx;
-          Monomorphic_entry Univ.ContextSet.empty
-        end
-  in
-  let fn status (id, b, t) =
-    let b, t = Option.map (to_constr sigma) b, to_constr sigma t in
-    if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
-      (* Declare the universe context once *)
-      let decl = match b with
-      | None ->
-        (ParameterEntry (None,(t,univs),None), IsAssumption Logical)
-      | Some b ->
-        let entry = Declare.definition_entry ~univs ~types:t b in
-        (DefinitionEntry entry, IsAssumption Logical)
-      in
-      let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
-        match class_of_constr sigma (of_constr t) with
-	| Some (rels, ((tc,_), args) as _cl) ->
-            add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (ConstRef cst));
-            status
-	    (* declare_subclasses (ConstRef cst) cl *)
-	| None -> status
-    else
-      let test (x, _) = match x with
-      | ExplByPos (_, Some id') -> Id.equal id id'
-      | _ -> false
-      in
-      let impl = List.exists test impls in
-      let decl = (Discharge, poly, Definitional) in
-      let nstatus = match b with
-      | None ->
-        pi3 (ComAssumption.declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl
-               Declaremods.NoInline (CAst.make id))
-      | Some b ->
-        let decl = (Discharge, poly, Definition) in
-        let entry = Declare.definition_entry ~univs ~types:t b in
-        let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in
-        Lib.sections_are_opened () || Lib.is_modtype_strict ()
-      in
-	status && nstatus
-  in
-  List.fold_left fn true (List.rev ctx)
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 73e4b024ef..e7f90ff306 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -22,6 +22,12 @@ val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a
 
 (** Instance declaration *)
 
+val declare_instance : ?warn:bool -> env -> Evd.evar_map ->
+                       hint_info option -> bool -> GlobRef.t -> unit
+(** 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 existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
 (** globality, reference, optional priority and pattern information *)
 
@@ -64,6 +70,12 @@ val declare_new_instance :
   Hints.hint_info_expr ->
   unit
 
+(** {6 Low level interface used by Add Morphism, do not use } *)
+val mk_instance : typeclass -> hint_info -> bool -> GlobRef.t -> instance
+val add_instance : instance -> unit
+
+val add_class : env -> Evd.evar_map -> typeclass -> unit
+
 (** Setting opacity *)
 
 val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
@@ -71,13 +83,3 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> u
 (** For generation on names based on classes only *)
 
 val id_of_class : typeclass -> Id.t
-
-(** Context command *)
-
-(** returns [false] if, for lack of section, it declares an assumption
-    (unless in a module type). *)
-val context
-  :  pstate:Proof_global.t option
-  -> Decl_kinds.polymorphic
-  -> local_binder_expr list
-  -> bool
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index d7bd64067b..3406b6276f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -22,6 +22,7 @@ open Decl_kinds
 open Pretyping
 open Entries
 
+module RelDecl = Context.Rel.Declaration
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
 let axiom_into_instance = ref false
@@ -59,7 +60,9 @@ match local with
   in
   let r = VarRef ident in
   let () = maybe_declare_manual_implicits true r imps in
-  let () = Typeclasses.declare_instance None true r in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let () = Classes.declare_instance env sigma None true r in
   let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
   (r,Univ.Instance.empty,true)
 
@@ -77,7 +80,9 @@ match local with
   let () = maybe_declare_manual_implicits false gr imps in
   let () = Declare.declare_univ_binders gr pl in
   let () = assumption_message ident in
-  let () = if do_instance then Typeclasses.declare_instance None false gr in
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  let () = if do_instance then Classes.declare_instance env sigma None false gr in
   let () = if is_coe then Class.try_add_new_coercion gr ~local p in
   let inst = match ctx with
     | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
@@ -173,7 +178,7 @@ let do_assumptions ~pstate ~program_mode kind nl l =
   let ubinders = Evd.universe_binders sigma in
   pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) ->
       let t = replace_vars subst t in
-      let refs, status' = declare_assumptions ~pstate idl is_coe kind (t,uctx) ubinders imps nl in
+      let refs, status' = declare_assumptions ~pstate  idl is_coe kind (t,uctx) ubinders imps nl in
       let subst' = List.map2
           (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
           idl refs
@@ -206,3 +211,94 @@ let do_primitive id prim typopt =
   in
   let _kn = declare_constant id.CAst.v (PrimitiveEntry entry,IsPrimitive) in
   Flags.if_verbose Feedback.msg_info Pp.(Id.print id.CAst.v ++ str " is declared")
+
+let named_of_rel_context l =
+  let open EConstr.Vars in
+  let open RelDecl in
+  let acc, ctx =
+    List.fold_right
+      (fun decl (subst, ctx) ->
+         let id = match get_name decl with Anonymous -> invalid_arg "named_of_rel_context" | Name id -> id in
+               let d = match decl with
+           | LocalAssum (_,t) -> id, None, substl subst t
+           | LocalDef (_,b,t) -> id, Some (substl subst b), substl subst t in
+               (EConstr.mkVar id :: subst, d :: ctx))
+      l ([], [])
+  in ctx
+
+let context ~pstate poly l =
+  let env = Global.env() in
+  let sigma = Evd.from_env env in
+  let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
+  (* Note, we must use the normalized evar from now on! *)
+  let sigma = Evd.minimize_universes sigma in
+  let ce t = Pretyping.check_evars env (Evd.from_env env) sigma t in
+  let () = List.iter (fun decl -> Context.Rel.Declaration.iter_constr ce decl) fullctx in
+  let ctx =
+    try named_of_rel_context fullctx
+    with e when CErrors.noncritical e ->
+      user_err Pp.(str "Anonymous variables not allowed in contexts.")
+  in
+  let univs =
+    match ctx with
+    | [] -> assert false
+    | [_] -> Evd.univ_entry ~poly sigma
+    | _::_::_ ->
+      if Lib.sections_are_opened ()
+      then
+        (* More than 1 variable in a section: we can't associate
+           universes to any specific variable so we declare them
+           separately. *)
+        begin
+          let uctx = Evd.universe_context_set sigma in
+          Declare.declare_universe_context poly uctx;
+          if poly then Polymorphic_entry ([||], Univ.UContext.empty)
+          else Monomorphic_entry Univ.ContextSet.empty
+        end
+      else if poly then
+        (* Multiple polymorphic axioms: they are all polymorphic the same way. *)
+        Evd.univ_entry ~poly sigma
+      else
+        (* Multiple monomorphic axioms: declare universes separately
+           to avoid redeclaring them. *)
+        begin
+          let uctx = Evd.universe_context_set sigma in
+          Declare.declare_universe_context poly uctx;
+          Monomorphic_entry Univ.ContextSet.empty
+        end
+  in
+  let fn status (id, b, t) =
+    let b, t = Option.map (EConstr.to_constr sigma) b, EConstr.to_constr sigma t in
+    if Lib.is_modtype () && not (Lib.sections_are_opened ()) then
+      (* Declare the universe context once *)
+      let decl = match b with
+      | None ->
+        (ParameterEntry (None,(t,univs),None), IsAssumption Logical)
+      | Some b ->
+        let entry = Declare.definition_entry ~univs ~types:t b in
+        (DefinitionEntry entry, IsAssumption Logical)
+      in
+      let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
+      let env = Global.env () in
+      Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst);
+      status
+    else
+      let test (x, _) = match x with
+      | Constrexpr.ExplByPos (_, Some id') -> Id.equal id id'
+      | _ -> false
+      in
+      let impl = List.exists test impls in
+      let decl = (Discharge, poly, Definitional) in
+      let nstatus = match b with
+      | None ->
+        pi3 (declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl
+               Declaremods.NoInline (CAst.make id))
+      | Some b ->
+        let decl = (Discharge, poly, Definition) in
+        let entry = Declare.definition_entry ~univs ~types:t b in
+        let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in
+        Lib.sections_are_opened () || Lib.is_modtype_strict ()
+      in
+        status && nstatus
+  in
+  List.fold_left fn true (List.rev ctx)
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 32914cc11b..7c64317b70 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -9,8 +9,6 @@
 (************************************************************************)
 
 open Names
-open Constr
-open Entries
 open Vernacexpr
 open Constrexpr
 open Decl_kinds
@@ -25,19 +23,13 @@ val do_assumptions
   -> (ident_decl list * constr_expr) with_coercion list
   -> bool
 
-(************************************************************************)
-(** Internal API  *)
-(************************************************************************)
-
-(** Exported for Classes *)
-
 (** returns [false] if the assumption is neither local to a section,
     nor in a module type and meant to be instantiated. *)
 val declare_assumption
   :  pstate:Proof_global.t option
   -> coercion_flag
   -> assumption_kind
-  -> types in_universes_entry
+  -> Constr.types Entries.in_universes_entry
   -> UnivNames.universe_binders
   -> Impargs.manual_implicits
   -> bool (** implicit *)
@@ -45,4 +37,14 @@ val declare_assumption
   -> variable CAst.t
   -> GlobRef.t * Univ.Instance.t * bool
 
+(** Context command *)
+
+(** returns [false] if, for lack of section, it declares an assumption
+    (unless in a module type). *)
+val context
+  :  pstate:Proof_global.t option
+  -> Decl_kinds.polymorphic
+  -> local_binder_expr list
+  -> bool
+
 val do_primitive : lident -> CPrimitives.op_or_type -> constr_expr option -> unit
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index d329b81341..082b22b373 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -601,7 +601,7 @@ let rec explain_evar_kind env sigma evk ty =
       (pr_leconstr_env env sigma ty') src
 
 let explain_typeclass_resolution env sigma evi k =
-  match Typeclasses.class_of_constr sigma evi.evar_concl with
+  match Typeclasses.class_of_constr env sigma evi.evar_concl with
   | Some _ ->
     let env = Evd.evar_filtered_env evi in
       fnl () ++ str "Could not find an instance for " ++
@@ -614,7 +614,7 @@ let explain_placeholder_kind env sigma c e =
   | Some (SeveralInstancesFound n) ->
       strbrk " (several distinct possible type class instances found)"
   | None ->
-      match Typeclasses.class_of_constr sigma c with
+      match Typeclasses.class_of_constr env sigma c with
       | Some _ -> strbrk " (no type class instance found)"
       | _ -> mt ()
 
diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 1e733acc59..642695bda4 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -313,7 +313,9 @@ let warn_cannot_build_congruence =
           strbrk "Cannot build congruence scheme because eq is not found")
 
 let declare_congr_scheme ind =
-  if Hipattern.is_equality_type Evd.empty (EConstr.of_constr (mkInd ind)) (* FIXME *) then begin
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
+  if Hipattern.is_equality_type env sigma (EConstr.of_constr (mkInd ind)) (* FIXME *) then begin
     if
       try Coqlib.check_required_library Coqlib.logic_module_name; true
       with e when CErrors.noncritical e -> false
diff --git a/vernac/record.ml b/vernac/record.ml
index cb67548667..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
@@ -520,8 +542,10 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
       List.map map inds
   in
   let ctx_context =
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
     List.map (fun decl ->
-      match Typeclasses.class_of_constr Evd.empty (EConstr.of_constr (RelDecl.get_type decl)) with
+      match Typeclasses.class_of_constr env sigma (EConstr.of_constr (RelDecl.get_type decl)) with
       | Some (_, ((cl,_), _)) -> Some cl.cl_impl
       | None -> None)
       params, params
@@ -548,12 +572,14 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity
         cl_props = fields;
         cl_projs = projs }
     in
-    add_class k; impl
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
+    Classes.add_class env sigma k; impl
   in
   List.map map data
 
 
-let add_constant_class env cst =
+let add_constant_class env sigma cst =
   let ty, univs = Typeops.type_of_global_in_context env (ConstRef cst) in
   let r = (Environ.lookup_constant cst env).const_relevance in
   let ctx, arity = decompose_prod_assum ty in
@@ -566,10 +592,11 @@ let add_constant_class env cst =
       cl_strict = !typeclasses_strict;
       cl_unique = !typeclasses_unique
     }
-  in add_class tc;
+  in
+  Classes.add_class env sigma tc;
     set_typeclass_transparency (EvalConstRef cst) false false
-      
-let add_inductive_class env ind =
+
+let add_inductive_class env sigma ind =
   let mind, oneind = Inductive.lookup_mind_specif env ind in
   let k =
     let ctx = oneind.mind_arity_ctxt in
@@ -586,7 +613,8 @@ let add_inductive_class env ind =
 	cl_projs = [];
 	cl_strict = !typeclasses_strict;
 	cl_unique = !typeclasses_unique }
-  in add_class k
+  in
+  Classes.add_class env sigma k
 
 let warn_already_existing_class =
   CWarnings.create ~name:"already-existing-class" ~category:"automation" Pp.(fun g ->
@@ -594,11 +622,12 @@ let warn_already_existing_class =
 
 let declare_existing_class g =
   let env = Global.env () in
+  let sigma = Evd.from_env env in
   if Typeclasses.is_class g then warn_already_existing_class g
   else
     match g with
-    | ConstRef x -> add_constant_class env x
-    | IndRef x -> add_inductive_class env x
+    | ConstRef x -> add_constant_class env sigma x
+    | IndRef x -> add_inductive_class env sigma x
     | _ -> user_err ~hdr:"declare_existing_class"
              (Pp.str"Unsupported class type, only constants and inductives are allowed")
 
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 ce93a8baaf..7f5c265eea 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -12,6 +12,7 @@ Vernacextend
 Ppvernac
 Proof_using
 Lemmas
+Canonical
 Class
 Egramcoq
 Metasyntax
@@ -21,11 +22,11 @@ Indschemes
 DeclareDef
 Obligations
 ComDefinition
+Classes
 ComAssumption
 ComInductive
 ComFixpoint
 ComProgramFixpoint
-Classes
 Record
 Assumptions
 Vernacstate
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index de8cdaa633..6c24b9ec75 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
@@ -1075,7 +1075,7 @@ let vernac_declare_instance ~atts sup inst pri =
   Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri
 
 let vernac_context ~pstate ~poly l =
-  if not (Classes.context ~pstate poly l) then Feedback.feedback Feedback.AddedAxiom
+  if not (ComAssumption.context ~pstate poly l) then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_existing_instance ~section_local insts =
   let glob = not section_local in