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

1 files changed, 4 insertions, 6 deletions

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