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. --- pretyping/inductiveops.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'pretyping/inductiveops.mli') diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index e375a2c6b..cf5523a50 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -185,8 +185,8 @@ val make_case_info : env -> inductive -> case_style -> case_info Fail with an error if the elimination is dependent while the inductive type does not allow dependent elimination. *) val make_case_or_project : - env -> inductive_family -> case_info -> - (* pred *) constr -> (* term *) constr -> (* branches *) constr array -> constr + env -> evar_map -> inductive_family -> case_info -> + (* pred *) EConstr.constr -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr (*i Compatibility val make_default_case_info : env -> case_style -> inductive -> case_info -- cgit v1.2.3