modules Indrec, Tacentries, Hiddentac

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

1 files changed, 3 insertions, 22 deletions

diff --git a/library/global.ml b/library/global.ml
index 63efdbe4d..e6c400806 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -1,6 +1,7 @@
 
 (* $Id$ *)
 
+open Util
 open Generic
 open Term
 open Instantiate
@@ -52,29 +53,9 @@ let mind_is_recursive = Util.compose mis_is_recursive lookup_mind_specif
 let mind_nconstr = Util.compose mis_nconstr lookup_mind_specif
 let mind_nparams = Util.compose mis_nparams lookup_mind_specif
 
-let mis_arity' mis =
-  let idhyps = ids_of_sign mis.mis_mib.mind_hyps 
-  and largs = Array.to_list mis.mis_args in 
-  { body = instantiate_constr idhyps mis.mis_mip.mind_arity.body largs;
-    typ = mis.mis_mip.mind_arity.typ }
-
-let mis_arity mispec =
-  let { body = b; typ = t } = mis_arity' mispec in
-  DOP2 (Cast, b, DOP0 (Sort t))
-
 let mind_arity = Util.compose mis_arity lookup_mind_specif
 
-let mis_lc mis = 
-  instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps)
-    mis.mis_mip.mind_lc (Array.to_list mis.mis_args)
-
-let mis_lc_without_abstractions mis = 
-  let rec strip_DLAM = function
-    | (DLAM (n,c1)) -> strip_DLAM c1 
-    | (DLAMV (n,v)) -> v
-    | _ -> assert false
-  in 
-  strip_DLAM (mis_lc mis)
-
 let mind_lc_without_abstractions = 
   Util.compose mis_lc_without_abstractions lookup_mind_specif
+
+