From 45562afa065aadc207dca4e904e309d835cb66ef Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 12 Nov 2016 01:28:45 +0100
Subject: Tacticals API using EConstr.

---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index fbf461f6f8..fa4164bb96 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -985,7 +985,7 @@ let apply_on_clause (f,t) clause =
   let t = EConstr.of_constr t in
   let f_clause = mk_clenv_from_env clause.env sigma None (f,t) in
   let argmv =
-    (match kind_of_term (last_arg f_clause.evd f_clause.templval.Evd.rebus) with
+    (match EConstr.kind sigma (last_arg f_clause.evd f_clause.templval.Evd.rebus) with
      | Meta mv -> mv
      | _  -> user_err  (str "Ill-formed clause applicator.")) in
   clenv_fchain ~with_univs:false argmv f_clause clause
-- 
cgit v1.2.3