diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-01-22 09:45:12 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-01-22 09:45:12 +0100 |
| commit | 35a275e22b72abba344b837e7276af8057d5da2c (patch) | |
| tree | d04e278cfc4a018be1a22b902aeeb8992027c760 /tactics/hipattern.ml | |
| parent | e0805eac59ee4c6c2eafae1d6b7f91530104f18f (diff) | |
| parent | d8652efca406c852ebc27cb27c903d9a6a4b2532 (diff) | |
Merge PR #6461: Let dtauto recognize '@sigT A (fun _ => B)' as a conjunction.
Diffstat (limited to 'tactics/hipattern.ml')
| -rw-r--r-- | tactics/hipattern.ml | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 11ac16680..2bb9be66b 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 *) |