From 6df4e0fe6bc6076bc95a1a71d28ae049d04ba517 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Thu, 10 Feb 2011 14:11:01 +0000
Subject: Data structure telling implicits of local variables is a map in the
 intern_env

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13823 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/indfun.ml | 4 ++--
 plugins/funind/recdef.ml | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index e571803273..38492f88b5 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -152,8 +152,8 @@ let build_newrecursive
         let arityc = Topconstr.prod_constr_expr arityc bl in
         let arity = Constrintern.interp_type sigma env0 arityc in
 	let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in
-        (Environ.push_named (recname,None,arity) env, (recname, impl) :: impls))
-      (env0,[]) lnameargsardef in
+        (Environ.push_named (recname,None,arity) env, Idmap.add recname impl impls))
+      (env0,Constrintern.empty_internalization_env) lnameargsardef in
   let recdef =
     (* Declare local notations *)
     let fs = States.freeze() in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index feff5d67c6..4217b83faf 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1410,7 +1410,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let equation_id = add_suffix function_name "_equation" in
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
-  let functional_ref = declare_fun functional_id (IsDefinition Definition) res in
+  let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) res in
   let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in  
   let relation =
     interp_constr
-- 
cgit v1.2.3