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.

---
 intf/tactypes.mli | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'intf')

diff --git a/intf/tactypes.mli b/intf/tactypes.mli
index b96cb67df8..02cfc44e29 100644
--- a/intf/tactypes.mli
+++ b/intf/tactypes.mli
@@ -26,8 +26,8 @@ type glob_constr_pattern_and_expr = Id.Set.t * glob_constr_and_expr * constr_pat
 type 'a delayed_open =
   { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma }
 
-type delayed_open_constr = Term.constr delayed_open
-type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open
+type delayed_open_constr = EConstr.constr delayed_open
+type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
 
 type intro_pattern = delayed_open_constr intro_pattern_expr located
 type intro_patterns = delayed_open_constr intro_pattern_expr located list
-- 
cgit v1.2.3