From 2d8dcd741d229c4de57ccce9f3ab09b808ccfc94 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Mon, 18 Dec 2017 21:51:25 +0900
Subject: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction

---
 tactics/hipattern.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index a3a3e0a9e9..28424c38ee 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -88,6 +88,12 @@ let is_lax_conjunction = function
 
 let prod_assum sigma t = fst (decompose_prod_assum sigma t)
 
+(* whd_beta normalize the types of arguments in a product *)
+let rec whd_beta_prod sigma c = match EConstr.kind sigma c with
+  | Prod (n,t,c) -> mkProd (n,Reductionops.whd_beta sigma t,whd_beta_prod sigma c)
+  | LetIn (n,d,t,c) -> mkLetIn (n,d,t,whd_beta_prod sigma c)
+  | _ -> c
+
 let match_with_one_constructor sigma style onlybinary allow_rec t =
   let (hdapp,args) = decompose_app sigma t in
   let res = match EConstr.kind sigma hdapp with
@@ -111,7 +117,8 @@ let match_with_one_constructor sigma style onlybinary allow_rec t =
 	    Some (hdapp,args)
 	  else None
 	else
-	  let ctyp = Termops.prod_applist sigma (EConstr.of_constr mip.mind_nf_lc.(0)) args in
+          let ctyp = whd_beta_prod sigma
+            (Termops.prod_applist sigma (EConstr.of_constr mip.mind_nf_lc.(0)) args) in
 	  let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in
 	  if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then
 	    (* Record or non strict conjunction *)
-- 
cgit v1.2.3