adapt test to use normal EWRSg again

javra · Mar 26, 2019 · a408320 · a408320
1 parent 2a370a3
commit a408320
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 4 deletions.
diff --git a/Test1.agda b/Test1.agda
@@ -5,7 +5,7 @@ module Test1 (C : Set) (Cw : C → Set)
  where
 
 open import II using (PS; P; S)
-open import EWRSgRec
+open import EWRSg
 open import Lib
 
 Γ : Con
@@ -20,7 +20,8 @@ open import Lib
 -}
 
 Γwc : _
-Γwc = Con.wc Γ (lift tt , C , T)
+Γwc = Con.wc Γ {lift tt , C , T}
+               (lift tt , n)
 
 Γw : _
 Γw = Con.w Γ {lift tt , C , T}

diff --git a/Test2.agda b/Test2.agda
@@ -1,7 +1,7 @@
 {-# OPTIONS --rewriting --allow-unsolved-metas #-}
 
 open import II using (PS; P; S)
-open import EWRSgRec
+open import EWRSg
 open import Lib
 
 module Test2
@@ -23,7 +23,8 @@ module Test2
 -}
 
 Γwc : _
-Γwc = Con.wc Γ (lift tt , C , T)
+Γwc = Con.wc Γ {lift tt , C , T}
+               (lift tt , e)
 
 Γw  : _
 Γw  = Con.w Γ {lift tt , C , T}