diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /test-suite/success/evars.v | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'test-suite/success/evars.v')
-rw-r--r-- | test-suite/success/evars.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v index 0f9fb745..253b48e4 100644 --- a/test-suite/success/evars.v +++ b/test-suite/success/evars.v @@ -386,7 +386,7 @@ Record iffT (X Y:Type) : Type := mkIff { iffLR : X->Y; iffRL : Y->X }. Record tri (R:Type->Type->Type) (S:Type->Type->Type) (T:Type->Type->Type) := mkTri { tri0 : forall a b c, R a b -> S a c -> T b c }. -Implicit Arguments mkTri [R S T]. +Arguments mkTri [R S T]. Definition tri_iffT : tri iffT iffT iffT := (mkTri (fun X0 X1 X2 E01 E02 => |