From 258c8502eafd3e078a5c7478a452432b5c046f71 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 19:59:28 +0100
Subject: Constr_matching API using EConstr.

---
 ltac/tactic_matching.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'ltac')

diff --git a/ltac/tactic_matching.ml b/ltac/tactic_matching.ml
index 43a58f6b2e..58998c96ed 100644
--- a/ltac/tactic_matching.ml
+++ b/ltac/tactic_matching.ml
@@ -233,7 +233,7 @@ module PatternMatching (E:StaticEnvironment) = struct
     | Term p ->
         begin 
           try
-            put_subst (Constr_matching.extended_matches E.env E.sigma p term) <*>
+            put_subst (Constr_matching.extended_matches E.env E.sigma p (EConstr.of_constr term)) <*>
             return lhs
           with Constr_matching.PatternMatchingFailure -> fail
         end
@@ -252,7 +252,7 @@ module PatternMatching (E:StaticEnvironment) = struct
             | Some nctx -> Proofview.tclOR (k lhs nctx) (fun e -> (map s e).stream k ctx)
         }
       in
-      map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p term) imatching_error
+      map (Constr_matching.match_subterm_gen E.env E.sigma with_app_context p (EConstr.of_constr term)) imatching_error
 
 
   (** [rule_match_term term rule] matches the term [term] with the
-- 
cgit v1.2.3