Compatibility with Agda 2.7/Stdlib 2.1.1

agda · Sep 10, 2024 · a4a279e · a4a279e
1 parent ac10c5a
commit a4a279e
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 3 deletions.
diff --git a/Class/MonadTC.agda b/Class/MonadTC.agda
@@ -106,13 +106,13 @@ record MonadTC (M : ∀ {f} → Set f → Set f)
   -- TODO: return true on function, axiom and prim-fun constructors?
   isDef : Name → M Bool
   isDef n = do
-    constructor′ _ ← getDefinition n
+    constructor′ _ _ ← getDefinition n
       where _ → return true
     return false
 
   isCon : Name → M Bool
   isCon n = do
-    constructor′ _ ← getDefinition n
+    constructor′ _ _ ← getDefinition n
       where _ → return false
     return true
 

diff --git a/README.md b/README.md
@@ -11,5 +11,7 @@ We mirror the version numbers of [agda-stdlib](https://github.com/agda/agda-stdl
 | [v2.6.3](https://github.com/agda/agda/releases/tag/v2.6.3) | [v1.7.2](https://github.com/agda/agda-stdlib/releases/tag/v1.7.2) | [v1.7.2](https://github.com/omelkonian/agda-stdlib-classes/releases/tag/v1.7.2) | [v1.7.2](https://github.com/omelkonian/agda-stdlib-meta/releases/tag/v1.7.2) |
 | [v2.6.4](https://github.com/agda/agda/releases/tag/v2.6.4) | [v1.7.3](https://github.com/agda/agda-stdlib/releases/tag/v1.7.3) | [v1.7.3](https://github.com/omelkonian/agda-stdlib-classes/releases/tag/v1.7.3) | [v1.7.3](https://github.com/omelkonian/agda-stdlib-meta/releases/tag/v1.7.3) |
 | [v2.6.4](https://github.com/agda/agda/releases/tag/v2.6.4) | [v2.0](https://github.com/agda/agda-stdlib/releases/tag/v2.0) | [v2.0](https://github.com/omelkonian/agda-stdlib-classes/releases/tag/v2.0) | [v2.0](https://github.com/omelkonian/agda-stdlib-meta/releases/tag/v2.0) |
+| [v2.6.4](https://github.com/agda/agda/releases/tag/v2.6.4) | [v2.0](https://github.com/agda/agda-stdlib/releases/tag/v2.1) | [v2.0](https://github.com/omelkonian/agda-stdlib-classes/releases/tag/v2.0) | [v2.0](https://github.com/omelkonian/agda-stdlib-meta/releases/tag/v2.1) |
+| [v2.7.0](https://github.com/agda/agda/releases/tag/v2.7.0) | [v2.1.1](https://github.com/agda/agda-stdlib/releases/tag/v2.0) | [v2.0](https://github.com/omelkonian/agda-stdlib-classes/releases/tag/v2.0) | [v2.1.1](https://github.com/omelkonian/agda-stdlib-meta/releases/tag/v2.1.1) |
 
 Minor revisions will append to these major versions (e.g. `v1.7.3b` or `v1.7.3.10`).
diff --git a/Tactic/Extra.agda b/Tactic/Extra.agda
@@ -169,7 +169,7 @@ getPatTele cn = do
   print $ "Getting pattern telescope for constructor: " ◇ show cn
   ty ← getType cn
   print $ "  ty: " ◇ show ty
-  data-cons n ← getDefinition cn
+  data-cons n _ ← getDefinition cn
     where _ → _IMPOSSIBLE_
   print $ "  n: " ◇ show n
   data-type ps _ ← getDefinition n