From e6a8ab0f428c26fff2bd7e636126974f167101bf Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 20 Nov 2016 01:35:54 +0100
Subject: Tactic_matching API using EConstr.

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

(limited to 'pretyping/constr_matching.mli')

diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 32bb48c93..4734c90a8 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -64,7 +64,7 @@ val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
    (whose hole is denoted here with [special_meta]) *)
 type matching_result =
     { m_sub : bound_ident_map * patvar_map;
-      m_ctx : Constr.t }
+      m_ctx : EConstr.t }
 
 (** [match_subterm n pat c] returns the substitution and the context
    corresponding to each **closed** subterm of [c] matching [pat]. *)
-- 
cgit v1.2.3