Remove some more "open" and dead code thanks to OCaml4 warnings

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15844 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 13 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 2817c549dd..fb9116cc2d 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -131,12 +131,6 @@ let coq_constant s =
   Coqlib.gen_constant_in_modules "RecursiveDefinition"
     Coqlib.init_modules s;;
 
-let constant sl s =
-  constr_of_global
-    (Nametab.locate (make_qualid(Names.make_dirpath
-			   (List.map id_of_string (List.rev sl)))
-	       (id_of_string s)));;
-
 let find_reference sl s =
     (Nametab.locate (make_qualid(Names.make_dirpath
 			   (List.map id_of_string (List.rev sl)))
@@ -277,7 +271,6 @@ let cache_Function (_,finfos) =
 
 
 let load_Function _  = cache_Function
-let open_Function _ = cache_Function
 let subst_Function (subst,finfos) =
   let do_subst_con c = fst (Mod_subst.subst_con subst c)
   and do_subst_ind (kn,i) = (Mod_subst.subst_ind subst kn,i)
@@ -508,12 +501,6 @@ let jmeq () =
      init_constant ["Logic";"JMeq"] "JMeq")
   with e -> raise (ToShow e)
 
-let jmeq_rec () =
-  try
-    Coqlib.check_required_library ["Coq";"Logic";"JMeq"];
-	  init_constant ["Logic";"JMeq"] "JMeq_rec"
-  with e -> raise (ToShow e)
-
 let jmeq_refl () =
   try
     Coqlib.check_required_library ["Coq";"Logic";"JMeq"];