From e22d8f725bae56550fed8cab8640447953cd3a47 Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Mon, 25 Feb 2019 00:04:44 +0100
Subject: [ssr] under: generate missing Under subgoal for eq_bigl/eq_big

in the particular case where the side-condition is phrased

  (_ : @eqfun bool I P1 P2)

instead of

  (_ : forall x : I, P1 x = P2 x)
---
 plugins/ssr/ssrfwd.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 570b5a8c61..491d6cfb33 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -360,6 +360,7 @@ let rec intro_lock names = Proofview.Goal.enter begin fun gl ->
   | Term.AtomicType _ ->
       let t = Reductionops.whd_all env sigma c in
       match EConstr.kind_of_type sigma t with
+      | Term.ProdType _ -> aux t
       | Term.AtomicType(hd, args) when
           Ssrcommon.is_ind_ref sigma hd (Coqlib.lib_ref "core.eq.type") &&
           Array.length args = 3 && is_app_evar sigma args.(2) ->
-- 
cgit v1.2.3