From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 20:09:26 +0100
Subject: Eliminating parts of the right-hand side compatibility layer

---
 plugins/decl_mode/decl_proof_instr.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 5de2c41517..e73166be28 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -786,7 +786,7 @@ let rec consider_match may_intro introduced available expected gls =
 
 let consider_tac c hyps gls =
   let c = EConstr.of_constr c in
-  match kind_of_term (strip_outer_cast (project gls) c) with
+  match EConstr.kind (project gls) (strip_outer_cast (project gls) c) with
       Var id ->
 	consider_match false [] [id] hyps gls
     | _ ->
@@ -811,6 +811,9 @@ let rec take_tac wits gls =
 
 (* tactics for define *)
 
+let subst_term sigma c t =
+  EConstr.Unsafe.to_constr (subst_term sigma c t)
+
 let rec build_function sigma args body =
   match args with
       st::rest ->
-- 
cgit v1.2.3