From 67dc22d8389234d0c9b329944ff579e7056b7250 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 8 Nov 2016 10:57:05 +0100 Subject: Cases API using EConstr. --- tactics/equality.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tactics/equality.ml') diff --git a/tactics/equality.ml b/tactics/equality.ml index 58c86ff42..9679ac402 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: -- cgit v1.2.3