From a5499688bd76def8de3d8e1089a49c7a08430903 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Nov 2016 14:54:40 +0100
Subject: Funind API using EConstr.

---
 plugins/funind/indfun.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/indfun.mli')

diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 1c27bdface..ba89fe4a78 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -12,8 +12,8 @@ val do_generate_principle :
 
 val functional_induction :  
   bool ->
-  Term.constr ->
-  (Term.constr * Term.constr bindings) option ->
+  EConstr.constr ->
+  (EConstr.constr * EConstr.constr bindings) option ->
   Tacexpr.or_and_intro_pattern option ->
   Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma
 
-- 
cgit v1.2.3