summaryrefslogtreecommitdiff
path: root/src/full/Agda/Auto/Convert.hs
diff options
context:
space:
mode:
Diffstat (limited to 'src/full/Agda/Auto/Convert.hs')
-rw-r--r--src/full/Agda/Auto/Convert.hs8
1 files changed, 6 insertions, 2 deletions
diff --git a/src/full/Agda/Auto/Convert.hs b/src/full/Agda/Auto/Convert.hs
index a12e5dd..13718e4 100644
--- a/src/full/Agda/Auto/Convert.hs
+++ b/src/full/Agda/Auto/Convert.hs
@@ -1,5 +1,9 @@
{-# LANGUAGE CPP #-}
+#if __GLASGOW_HASKELL__ >= 710
+{-# LANGUAGE FlexibleContexts #-}
+#endif
+
module Agda.Auto.Convert where
import Control.Applicative hiding (getConst, Const(..))
@@ -462,7 +466,7 @@ fmLevel :: I.MetaId -> I.PlusLevel -> Bool
fmLevel m I.ClosedLevel{} = False
fmLevel m (I.Plus _ l) = case l of
I.MetaLevel m' _ -> m == m'
- I.NeutralLevel v -> fmExp m v
+ I.NeutralLevel _ v -> fmExp m v
I.BlockedLevel _ v -> fmExp m v
I.UnreducedLevel v -> fmExp m v
@@ -667,7 +671,7 @@ frommyClause (ids, pats, mrhs) = do
let (Just ndrop, name) = cdorigin cdef
ps' <- cnvps ndrop ps
let con = I.ConHead name Common.Inductive [] -- TODO: restore record fields!
- return (I.ConP con Nothing ps')
+ return (I.ConP con I.noConPatternInfo ps')
CSPatExp e -> do
e' <- frommyExp e {- renm e -} -- renaming before adding to clause below
return (I.DotP e')