From 70bc1e9c5122ad5a8a3dc78aae764afc65b4dead Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 15 Feb 2020 11:56:40 +0100
Subject: Actually use the binder type for Ltac2 that should be used in the
 kernel.

That is, it contains the type of the binder so as not to rely on the relevance
explicitly.
---
 test-suite/ltac2/constr.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/ltac2/constr.v b/test-suite/ltac2/constr.v
index 39601d99a8..018596ed95 100644
--- a/test-suite/ltac2/constr.v
+++ b/test-suite/ltac2/constr.v
@@ -2,11 +2,11 @@ Require Import Ltac2.Constr Ltac2.Init Ltac2.Control.
 Import Unsafe.
 
 Ltac2 Eval match (kind '(nat -> bool)) with
-           | Prod a b c => a
+           | Prod a c => a
            | _ => throw Match_failure end.
 
 Set Allow StrictProp.
 Axiom something : SProp.
 Ltac2 Eval match (kind '(forall x : something, bool)) with
-           | Prod a b c => a
+           | Prod a c => a
            | _ => throw Match_failure end.
-- 
cgit v1.2.3