From cbea91d815f134d63d02d8fb1bd78ed97db28cd1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Fri, 11 Nov 2016 19:52:48 +0100
Subject: Tacmach API using EConstr.

---
 plugins/ssrmatching/ssrmatching.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/ssrmatching')

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 7f628f165..ace557a52 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1390,7 +1390,7 @@ let ssrpatterntac _ist (arg_ist,arg) gl =
   let concl0 = pf_concl gl in
   let (t, uc), concl_x =
     fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in
-  let gl, tty = pf_type_of gl t in
+  let gl, tty = pf_type_of gl (EConstr.of_constr t) in
   let concl = mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in
   Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl
 
-- 
cgit v1.2.3