From 888aaeb0a948352cf56f1f6d8023a051e90583a0 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 14 May 2020 14:46:56 +0200
Subject: Fix #11761: Functional Induction throws unrecoverable error.

Error happened only when writing:

functional induction f x y z.

instead of

functional induction (f x y z).

Now the former is equivalent to the former: implicits must be omitted.
Hence small source of incompatibility, but a more homogeneous
behaviour.
---
 test-suite/success/Funind.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'test-suite')

diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index f87f2e2a9d..e371cf251f 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -77,7 +77,7 @@ Functional Scheme app_ind := Induction for app Sort Prop.
 
 Lemma appnil : forall (A : Set) (l l' : list A), l' = nil -> l = l ++ l'.
 intros A l l'.
- functional induction app A l l';  intuition.
+ functional induction app l l';  intuition.
  rewrite <- H0; trivial.
 Qed.
 
-- 
cgit v1.2.3