Use instantiateCtxVar

Beluga-lang · Dec 21, 2023 · e16cc7b · e16cc7b
1 parent 8a74a07
commit e16cc7b
Showing 1 changed file with 10 additions and 5 deletions.
diff --git a/src/core/unify.ml b/src/core/unify.ml
@@ -3154,7 +3154,8 @@ let rec blockdeclInDctx =
               in
               (* why do we drop the constraints here ? -je *)
               let i = CInst (mmvar2', Whnf.mcomp theta2 mtt1) in
-              mmvar1.instantiation := Some (ICtx (CtxVar i))
+              let cPsi = CtxVar i in
+              instantiateCtxVar (mmvar1.instantiation, cPsi)
             end
           else
             Error.raise_violation
@@ -3164,26 +3165,30 @@ let rec blockdeclInDctx =
 
        | (Some c_var, d') ->
           if d = d'
-          then mmvar1.instantiation := Some (ICtx (CtxVar (c_var)))
+          then
+            let cPsi = CtxVar c_var in
+            instantiateCtxVar (mmvar1.instantiation, cPsi)
           else if d' < d
           then fail "Hat Context's do not unify"
           else
             begin
               let cPsi = Context.hatToDCtx (Some c_var, d' - d) in
-              mmvar1.instantiation := Some (ICtx cPsi)
+              instantiateCtxVar (mmvar1.instantiation, cPsi)
             end
 
        | (None, d') ->
           if d = d'
-          then mmvar1.instantiation := Some (ICtx Null)
+          then
+            let cPsi = Null in
+            instantiateCtxVar (mmvar1.instantiation, cPsi)
           else if d' < d
           then
             (* (Some (cref), d) == (None, d') d' = d0 + d *)
             fail "Hat Context's do not unify"
           else
             begin
               let cPsi = Context.hatToDCtx (None, d' - d) in
-              mmvar1.instantiation := Some (ICtx cPsi)
+              instantiateCtxVar (mmvar1.instantiation, cPsi)
             end
        end