From d833b81b49366e95cf20a1d00f9c63883adb8942 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 03:04:13 +0100
Subject: Rewrite API using EConstr.

---
 plugins/decl_mode/decl_proof_instr.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

(limited to 'plugins/decl_mode')

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 54206aa955..5de2c41517 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -382,6 +382,9 @@ let enstack_subsubgoals env se stack gls=
 	    Array.iteri process gentypes
       | _ -> ()
 
+let nf_meta sigma c =
+  EConstr.Unsafe.to_constr (Reductionops.nf_meta sigma (EConstr.of_constr c))
+
 let rec nf_list evd =
   function
       [] -> []
@@ -389,7 +392,7 @@ let rec nf_list evd =
 	if meta_defined evd m then
 	    nf_list evd others
 	else
-	  (m,Reductionops.nf_meta evd typ)::nf_list evd others
+	  (m,nf_meta evd typ)::nf_list evd others
 
 let find_subsubgoal c ctyp skip submetas gls =
   let env= pf_env gls in
@@ -424,7 +427,7 @@ let find_subsubgoal c ctyp skip submetas gls =
 	  dfs n
 	end in
   let nse= try dfs skip with Stack.Empty -> raise Not_found in
-    nf_list nse.se_evd nse.se_meta_list,Reductionops.nf_meta nse.se_evd (mkMeta 0)
+    nf_list nse.se_evd nse.se_meta_list,nf_meta nse.se_evd (mkMeta 0)
 
 let concl_refiner metas body gls =
   let concl = pf_concl gls in
-- 
cgit v1.2.3