From b1aa5d4583f2c3523b27330f8808f883d0bc8e5a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 5 Jul 2020 00:20:12 +0200
Subject: Do not look for a quantified inductive type in intropattern
 injection.

The code below checks that the term is an applied equality, so allowing
non-trivially quantified inductive types would trigger an error right after.
---
 tactics/tactics.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index eb7b7e363f..3b2481bc69 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2330,7 +2330,7 @@ let intro_decomp_eq ?loc l thin tac id =
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
   let sigma, t = Typing.type_of env sigma c in
-  let _,t = reduce_to_quantified_ind env sigma t in
+  let _,t = reduce_to_atomic_ind env sigma t in
   match my_find_eq_data_decompose env sigma t with
   | Some (eq,u,eq_args) ->
     !intro_decomp_eq_function
-- 
cgit v1.2.3