Changing the definition of the "Lib.variable.info" type to enable us to do more cleanups

2 files changed, 5 insertions, 7 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index ca1d0b7fba..bf9063fdbc 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -48,7 +48,7 @@ let discharge_rename_args = function
      (try 
        let vars,_,_ = section_segment_of_reference c in
        let c' = pop_global_reference c in
-       let var_names = List.map (fun (id, _,_,_) -> Name id) vars in
+       let var_names = List.map (Name.mk_name % Context.Named.Declaration.get_id % fst) vars in
        let names' = List.map (fun l -> var_names @ l) names in
        Some (ReqGlobal (c', names), (c', names'))
      with Not_found -> Some req)
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2c675b9eae..9fff64ae51 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -197,12 +197,10 @@ let subst_class (subst,cl) =
 let discharge_class (_,cl) =
   let repl = Lib.replacement_context () in
   let rel_of_variable_context ctx = List.fold_right
-    ( fun (n,_,b,t) (ctx', subst) ->
-        let decl = match b with
-                   | None -> LocalAssum (Name n, substn_vars 1 subst t)
-		   | Some b -> LocalDef (Name n, substn_vars 1 subst b, substn_vars 1 subst t)
-	in
-	(decl :: ctx', n :: subst)
+    ( fun (decl,_) (ctx', subst) ->
+        let open Context.Named.Declaration in
+        let decl' = decl |> map_constr (substn_vars 1 subst) |> to_rel in
+	(decl' :: ctx', Context.Named.Declaration.get_id decl :: subst)
     ) ctx ([], []) in
   let discharge_rel_context subst n rel =
     let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in