From 71a579d3bb053e686a92aec111f847bb61f4d8a8 Mon Sep 17 00:00:00 2001
From: Julien Forest
Date: Mon, 22 Sep 2014 14:20:03 +0200
Subject: Fixing bug 3951

---
 plugins/funind/indfun.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index be84f2ed44..b613a4b13c 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -149,7 +149,9 @@ let build_newrecursive
       (fun (env,impls) ((_,recname),bl,arityc,_) ->
         let arityc = Constrexpr_ops.prod_constr_expr arityc bl in
         let arity,ctx = Constrintern.interp_type env0 sigma arityc in
-	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
+	let evdref =  ref (Evd.from_env env0) in
+	let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in
+	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in
         (Environ.push_named (recname,None,arity) env, Id.Map.add recname impl impls))
       (env0,Constrintern.empty_internalization_env) lnameargsardef in
   let recdef =
-- 
cgit v1.2.3