diff options
| author | Pierre-Marie Pédrot | 2020-02-15 11:56:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-18 18:24:44 +0100 |
| commit | 70bc1e9c5122ad5a8a3dc78aae764afc65b4dead (patch) | |
| tree | 68396484f0a62cdf55dc8e0723d67743c102e68f /test-suite | |
| parent | 9d533d1b851b9504599778a77dd32724d6b39219 (diff) | |
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.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/ltac2/constr.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |