diff options
| author | Pierre-Marie Pédrot | 2016-11-08 10:57:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:27:23 +0100 |
| commit | 67dc22d8389234d0c9b329944ff579e7056b7250 (patch) | |
| tree | 4b0d94384103f34e8b6071a214efb84904a56277 /tactics | |
| parent | e4f066238799a4598817dfeab8a044760ab670de (diff) | |
Cases API using EConstr.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 2 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 58c86ff426..9679ac4026 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -864,7 +864,7 @@ let descend_then env sigma head dirn = List.map build_branch (List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in - Inductiveops.make_case_or_project env indf ci p head (Array.of_list brl))) + EConstr.Unsafe.to_constr (Inductiveops.make_case_or_project env sigma indf ci (EConstr.of_constr p) (EConstr.of_constr head) (Array.map_of_list EConstr.of_constr brl)))) (* Now we need to construct the discriminator, given a discriminable position. This boils down to: diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index d27e4afb74..87e252a380 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 |