From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 13 Nov 2016 20:38:41 +0100
Subject: Tactics API using EConstr.

---
 pretyping/inductiveops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/inductiveops.mli')

diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index cf5523a50d..7af9731f9a 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -175,7 +175,7 @@ val arity_of_case_predicate :
   env -> inductive_family -> bool -> sorts -> types
 
 val type_case_branches_with_names :
-  env -> evar_map -> pinductive * constr list -> constr -> constr -> types array * types
+  env -> evar_map -> pinductive * EConstr.constr list -> constr -> constr -> types array * types
 
 (** Annotation for cases *)
 val make_case_info : env -> inductive -> case_style -> case_info
-- 
cgit v1.2.3