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/pattern.mli')

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