From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 13 Nov 2016 20:38:41 +0100
Subject: Tactics API using EConstr.

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

(limited to 'plugins/ssrmatching')

diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index ace557a52..aa91494eb 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1392,6 +1392,7 @@ let ssrpatterntac _ist (arg_ist,arg) gl =
     fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 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
+  let concl = EConstr.of_constr concl in
   Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl
 
 (* Register "ssrpattern" tactic *)
-- 
cgit v1.2.3