fix indentation

GaloisInc · May 10, 2021 · f10786a · f10786a
1 parent c71afc8
commit f10786a
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/src/Verifier/SAW/Heapster/Implication.hs b/src/Verifier/SAW/Heapster/Implication.hs
@@ -5901,7 +5901,7 @@ proveVarLLVMBlocks' x ps psubst mb_bps_in mb_ps = case mbMatch mb_bps_in of
       implSplitSwapConjsM x ps' 1 >>>
 
       -- Prove an existential around the memblock permission we proved
-       partialSubstForceM (mbMap2 (,)
+      partialSubstForceM (mbMap2 (,)
                           mb_bp mb_mb_sh) "proveVarLLVMBlock" >>>= \(bp,mb_sh) ->
       introExistsM x e (fmap (\sh -> ValPerm_LLVMBlock $
                                      bp { llvmBlockShape = sh }) mb_sh) >>>

diff --git a/src/Verifier/SAW/Heapster/SAWTranslation.hs b/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -2991,8 +2991,8 @@ translatePermImplUnary ::
   Mb ctx (MbPermImpls r (RNil :> '(bs,ps_out))) ->
   (ImpTransM ext blocks tops ret ps_out (ctx :++: bs) OpenTerm ->
    ImpTransM ext blocks tops ret ps ctx OpenTerm) ->
-  PermImplTransM (ImplFailCont ->
-  ImpTransM ext blocks tops ret ps ctx OpenTerm)
+  PermImplTransM
+    (ImplFailCont -> ImpTransM ext blocks tops ret ps ctx OpenTerm)
 translatePermImplUnary (mbMatch -> [nuMP| MbPermImpls_Cons _ _ mb_impl |]) f =
   translatePermImpl Proxy (mbCombine RL.typeCtxProxies mb_impl) >>= \trans ->
   return $ \k -> f $ trans k