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


From e6a8ab0f428c26fff2bd7e636126974f167101bf Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 01:35:54 +0100
Subject: Tactic_matching API using EConstr.

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

(limited to 'intf')

diff --git a/intf/pattern.mli b/intf/pattern.mli
index 329ae837e1..ac84b91e68 100644
--- a/intf/pattern.mli
+++ b/intf/pattern.mli
@@ -43,11 +43,11 @@ open Misctypes
     could be inferred. We also loose the ability of typing ltac
     variables before calling the right-hand-side of ltac matching clauses. *)
 
-type constr_under_binders = Id.t list * constr
+type constr_under_binders = Id.t list * EConstr.constr
 
 (** Types of substitutions with or w/o bound variables *)
 
-type patvar_map = constr Id.Map.t
+type patvar_map = EConstr.constr Id.Map.t
 type extended_patvar_map = constr_under_binders Id.Map.t
 
 (** {5 Patterns} *)
-- 
cgit v1.2.3