Fix #664. (#679)

RedPRL · Apr 20, 2018 · 59075c7 · 59075c7
1 parent 03bb5b0
commit 59075c7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/redprl/refiner_composition_kit.fun b/src/redprl/refiner_composition_kit.fun
@@ -168,7 +168,7 @@ struct
         val _ = Assert.tautologicalEquations "HCom.Eq tautology checking" eqs0
 
         (* type *)
-        val goalTy0 = makeType tr H (ty0, k)
+        val goalTy0 = makeEqType tr H ((ty0, ty1), k)
         val goalTy = View.makeAsSubTypeIfDifferent tr H (ty0, ty) (* (ty0, k) is proved *)
 
         (* cap *)