diff options
Diffstat (limited to 'kernel/term.ml')
| -rw-r--r-- | kernel/term.ml | 43 |
1 files changed, 0 insertions, 43 deletions
diff --git a/kernel/term.ml b/kernel/term.ml index 492ebbb0d..88bc4cc4e 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -285,14 +285,6 @@ let kind_of_term2 c = c let kind_of_term = kind_of_term - -(* En vue d'un kind_of_type : constr -> hnftype ??? *) -type hnftype = - | HnfSort of sorts - | HnfProd of name * constr * constr - | HnfAtom of constr - | HnfInd of inductive * constr array - (**********************************************************************) (* Non primitive term destructors *) (**********************************************************************) @@ -346,18 +338,12 @@ let rec is_Type c = match kind_of_term c with | Cast (c,_,_) -> is_Type c | _ -> false -let isType = function - | Type _ -> true - | _ -> false - let is_small = function | Prop _ -> true | _ -> false let iskind c = isprop c or is_Type c -let same_kind c1 c2 = (isprop c1 & isprop c2) or (is_Type c1 & is_Type c2) - (* Tests if an evar *) let isEvar c = match kind_of_term c with Evar _ -> true | _ -> false @@ -424,10 +410,6 @@ let destEvar c = match kind_of_term c with | Evar (kn, a as r) -> r | _ -> invalid_arg "destEvar" -let num_of_evar c = match kind_of_term c with - | Evar (n, _) -> n - | _ -> anomaly "num_of_evar called with bad args" - (* Destructs a (co)inductive type named kn *) let destInd c = match kind_of_term c with | Ind (kn, a as r) -> r @@ -497,18 +479,6 @@ let decompose_app c = | App (f,cl) -> (f, Array.to_list cl) | _ -> (c,[]) -(* strips head casts and flattens head applications *) -let rec strip_head_cast c = match kind_of_term c with - | App (f,cl) -> - let rec collapse_rec f cl2 = match kind_of_term f with - | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) - | Cast (c,_,_) -> collapse_rec c cl2 - | _ -> if Array.length cl2 = 0 then f else mkApp (f,cl2) - in - collapse_rec f cl - | Cast (c,_,_) -> strip_head_cast c - | _ -> c - (****************************************************************************) (* Functions to recur through subterms *) (****************************************************************************) @@ -899,12 +869,10 @@ let mkCast = mkCast (* Constructs the product (x:t1)t2 *) let mkProd = mkProd let mkNamedProd id typ c = mkProd (Name id, typ, subst_var id c) -let mkProd_string s t c = mkProd (Name (id_of_string s), t, c) (* Constructs the abstraction [x:t1]t2 *) let mkLambda = mkLambda let mkNamedLambda id typ c = mkLambda (Name id, typ, subst_var id c) -let mkLambda_string s t c = mkLambda (Name (id_of_string s), t, c) (* Constructs [x=c_1:t]c_2 *) let mkLetIn = mkLetIn @@ -933,11 +901,6 @@ let mkNamedLambda_or_LetIn (id,body,t) c = | Some b -> mkNamedLetIn id b t c (* Constructs either [(x:t)c] or [c] where [x] is replaced by [b] *) -let mkProd_wo_LetIn (na,body,t) c = - match body with - | None -> mkProd (na, t, c) - | Some b -> subst1 b c - let mkNamedProd_wo_LetIn (id,body,t) c = match body with | None -> mkNamedProd id t c @@ -951,11 +914,6 @@ let mkArrow t1 t2 = mkProd (Anonymous, t1, t2) function is not itself an applicative term *) let mkApp = mkApp -let mkAppA v = - let l = Array.length v in - if l=0 then anomaly "mkAppA received an empty array" - else mkApp (v.(0), Array.sub v 1 (Array.length v -1)) - (* Constructs a constant *) (* The array of terms correspond to the variables introduced in the section *) let mkConst = mkConst @@ -974,7 +932,6 @@ let mkConstruct = mkConstruct (* Constructs the term <p>Case c of c1 | c2 .. | cn end *) let mkCase = mkCase -let mkCaseL (ci, p, c, ac) = mkCase (ci, p, c, Array.of_list ac) (* If recindxs = [|i1,...in|] funnames = [|f1,...fn|] |