diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-08 10:57:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:27:23 +0100 |
| commit | 67dc22d8389234d0c9b329944ff579e7056b7250 (patch) | |
| tree | 4b0d94384103f34e8b6071a214efb84904a56277 /tactics/hipattern.ml | |
| parent | e4f066238799a4598817dfeab8a044760ab670de (diff) | |
Cases API using EConstr.
Diffstat (limited to 'tactics/hipattern.ml')
| -rw-r--r-- | tactics/hipattern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index d27e4afb7..87e252a38 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -110,7 +110,7 @@ let match_with_one_constructor sigma style onlybinary allow_rec t = Some (hdapp,args) else None else - let ctyp = prod_applist mip.mind_nf_lc.(0) args in + let ctyp = Term.prod_applist mip.mind_nf_lc.(0) args in let cargs = List.map RelDecl.get_type (prod_assum ctyp) in if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then (* Record or non strict conjunction *) @@ -176,7 +176,7 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = None else let cargs = - Array.map (fun ar -> pi2 (destProd (prod_applist ar args))) + Array.map (fun ar -> pi2 (destProd (Term.prod_applist ar args))) mip.mind_nf_lc in Some (hdapp,Array.to_list cargs) else |