5602ea7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

A small cleanup after missing some stray ends in the diff.

commit5602ea7a47b90807fc7376b970c8169262e75884 authorDominic Mulligan <dominic.p.mulligan@googlemail.com> dateThu 1 Mar 2012, 14:41 (15 years ago) parent2ba8712

3 files changed+3−5

compare with master

unifiedsplit

src/Core/Elaborate.hs+1−3 src/Core/ProofShell.hs+1−1 src/Core/TT.hs+1−1

src/Core/Elaborate.hs+1−3

@@ -31,9 +31,7 @@ data Command = Theorem Name Raw

3131 | Tac (Elab ())

3232

3333data ElabState aux = ES (ProofState, aux) String (Maybe (ElabState aux))

34−

35−instance Pretty aux => Pretty (ElabState aux) where

36− pretty (ES (pState, aux) str _) = text "test"

34+ deriving Show

3735

3836type Elab' aux a = StateT (ElabState aux) TC a

3937type Elab a = Elab' () a

src/Core/ProofShell.hs+1−1

@@ -52,7 +52,7 @@ processCommand (Tac e) state

5252 (pterm ps')

5353 (ptype ps')

5454 (context ps') }, resp)

55− err -> (state, show . render . pretty $ err)

55+ err -> (state, show err)

5656 | otherwise = (state, "No proof in progress")

5757

5858runShell :: ShellState -> InputT IO ShellState

src/Core/TT.hs+1−1

@@ -1,4 +1,4 @@

1−{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor, FlexibleInstances #-}

1+{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies, DeriveFunctor #-}

33module Core.TT where