06bfa75 · Idris-dev · git.iko.soy

CHANGELOG+1

@@ -8,6 +8,7 @@ Internal changes:

8* Change unification so that it keeps track of failed constraints in case

9 later information helps to resolve them

10* Distinguishing parameters and indices in data types

11+* Faster termination/coverage checking

11

12

12New in 0.9.6:

13New in 0.9.6:

13-------------

14-------------

src/Core/Typecheck.hs+2−2

@@ -29,10 +29,10 @@ convertsC ctxt env x y

29converts :: Context -> Env -> Term -> Term -> TC ()

30converts ctxt env x y

31 = case convEq' ctxt x y of

32− OK _ -> return ()

32+ OK True -> return ()

33 _ -> case convEq' ctxt (finalise (normalise ctxt env x))

34 (finalise (normalise ctxt env y)) of

35− OK _ -> return ()

35+ OK True -> return ()

36 _ -> tfail (CantConvert

37 (finalise (normalise ctxt env x))

38 (finalise (normalise ctxt env y)) (errEnv env))

src/Idris/ElabDecls.hs+1−1

@@ -557,7 +557,7 @@ elabClause info tcgen (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

557 logLvl 3 ("Elaborated: " ++ show lhs_tm)

558 logLvl 3 ("Elaborated type: " ++ show lhs_ty)

559 (clhs, clhsty) <- recheckC fc [] lhs_tm

560− logLvl 5 ("Checked " ++ show clhs)

560+ logLvl 5 ("Checked " ++ show clhs ++ "\n" ++ show clhsty)

561 -- Elaborate where block

562 ist <- getIState

563 windex <- getName

test/test002/run+1−1

@@ -1,3 +1,3 @@

1#!/bin/bash

2idris $@ test002.idr --check --noprelude

3−

3+rm -f *.ibc