Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.

3 files changed, 22 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 7fe5b91f5d..8c9b51b86b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -42,6 +42,8 @@ Tactics
   in the OCaml run-time system.
 - The tactics "dtauto", "dintuition", "firstorder" now handle inductive types
   with let bindings in the parameters.
+- The tactic "dtauto" now handles some inductives such as
+  "@sigT A (fun _ => B)" as non-dependent conjunctions.
 
 Focusing
 
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index 11ac166801..2bb9be66ba 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,8 +117,9 @@ let match_with_one_constructor sigma style onlybinary allow_rec t =
 	    Some (hdapp,args)
 	  else None
 	else
-          let ctyp = Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt)
-                       (EConstr.of_constr mip.mind_nf_lc.(0)) args in
+          let ctyp = whd_beta_prod sigma
+            (Termops.prod_applist_assum sigma (Context.Rel.length mib.mind_params_ctxt)
+                       (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 *)
diff --git a/test-suite/bugs/opened/6393.v b/test-suite/bugs/opened/6393.v
new file mode 100644
index 0000000000..8d5d092333
--- /dev/null
+++ b/test-suite/bugs/opened/6393.v
@@ -0,0 +1,11 @@
+(* These always worked. *)
+Goal prod True True. firstorder. Qed.
+Goal True -> @sigT True (fun _ => True). firstorder. Qed.
+Goal prod True True. dtauto. Qed.
+Goal prod True True. tauto. Qed.
+
+(* These should work. *)
+Goal @sigT True (fun _ => True). dtauto. Qed.
+(* These should work, but don't *)
+(* Goal @sigT True (fun _ => True). firstorder. Qed. *)
+(* Goal @sigT True (fun _ => True). tauto. Qed. *)