From 69929de6eccf6d60886ea0795376e9288863fc1f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:08:17 +0000
Subject: Decl_kinds becomes a pure mli file, remaining ops in new file
 kindops.ml

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15368 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/funind/indfun_common.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 60aa99b124..de7e179571 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -163,16 +163,16 @@ let save with_clean id const (locality,kind) hook =
        const_entry_opaque = opacity } = const in
   let l,r = match locality with
     | Local when Lib.sections_are_opened () ->
-        let k = logical_kind_of_goal_kind kind in
+        let k = Kindops.logical_kind_of_goal_kind kind in
 	let c = SectionLocalDef (pft, tpo, opacity) in
 	let _ = declare_variable id (Lib.cwd(), c, k) in
 	(Local, VarRef id)
     | Local ->
-        let k = logical_kind_of_goal_kind kind in
+        let k = Kindops.logical_kind_of_goal_kind kind in
         let kn = declare_constant id (DefinitionEntry const, k) in
 	(Global, ConstRef kn)
     | Global ->
-        let k = logical_kind_of_goal_kind kind in
+        let k = Kindops.logical_kind_of_goal_kind kind in
         let kn = declare_constant id (DefinitionEntry const, k) in
 	(Global, ConstRef kn) in
   if with_clean then  Pfedit.delete_current_proof ();
-- 
cgit v1.2.3