From 771be16883c8c47828f278ce49545716918764c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 12 Nov 2016 01:52:15 +0100
Subject: Hipattern API using EConstr.

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

(limited to 'tactics/tactics.mli')

diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 268453152..368a1df76 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -413,7 +413,7 @@ val subst_one :
 
 val declare_intro_decomp_eq :
   ((int -> unit Proofview.tactic) -> Coqlib.coq_eq_data * types *
-   (types * constr * constr) ->
+   (EConstr.types * EConstr.constr * EConstr.constr) ->
    constr * types -> unit Proofview.tactic) -> unit
 
 (** {6 Simple form of basic tactics. } *)
-- 
cgit v1.2.3