diff options
| -rw-r--r-- | tactics/hipattern.ml | 9 | ||||
| -rw-r--r-- | test-suite/bugs/opened/6393.v | 11 |
2 files changed, 19 insertions, 1 deletions
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 *) 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. *) |