diff options
Diffstat (limited to 'kernel/sign.mli')
| -rw-r--r-- | kernel/sign.mli | 44 |
1 files changed, 1 insertions, 43 deletions
diff --git a/kernel/sign.mli b/kernel/sign.mli index 88e9dbf0..b3e7ace5 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: sign.mli 9103 2006-09-01 11:02:52Z herbelin $ i*) +(*i $Id$ i*) (*i*) open Names @@ -40,16 +40,6 @@ val instance_from_named_context : named_context -> constr array (*s Signatures of ordered optionally named variables, intended to be accessed by de Bruijn indices *) -(* In [rel_context], more recent declaration is on top *) -type rel_context = rel_declaration list - -val empty_rel_context : rel_context -val add_rel_decl : rel_declaration -> rel_context -> rel_context - -val lookup_rel : int -> rel_context -> rel_declaration -val rel_context_length : rel_context -> int -val rel_context_nhyps : rel_context -> int - val push_named_to_rel_context : named_context -> rel_context -> rel_context (*s Recurrence on [rel_context]: older declarations processed first *) @@ -70,35 +60,3 @@ val iter_rel_context : (constr -> unit) -> rel_context -> unit (*s Map function of [named_context] *) val iter_named_context : (constr -> unit) -> named_context -> unit - -(*s Term constructors *) - -val it_mkLambda_or_LetIn : constr -> rel_context -> constr -val it_mkProd_or_LetIn : types -> rel_context -> types - -(*s Term destructors *) - -(* Destructs a term of the form $(x_1:T_1)..(x_n:T_n)s$ into the pair *) -type arity = rel_context * sorts -val destArity : types -> arity -val mkArity : arity -> types -val isArity : types -> bool - -(* Transforms a product term $(x_1:T_1)..(x_n:T_n)T$ including letins - into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a - product nor a let. *) -val decompose_prod_assum : types -> rel_context * types - -(* Transforms a lambda term $[x_1:T_1]..[x_n:T_n]T$ including letins - into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$, where $T$ is not a - lambda nor a let. *) -val decompose_lam_assum : constr -> rel_context * constr - -(* Given a positive integer n, transforms a product term - $(x_1:T_1)..(x_n:T_n)T$ - into the pair $([(xn,Tn);...;(x1,T1)],T)$. *) -val decompose_prod_n_assum : int -> types -> rel_context * types - -(* Given a positive integer $n$, transforms a lambda term - $[x_1:T_1]..[x_n:T_n]T$ into the pair $([(x_n,T_n);...;(x_1,T_1)],T)$ *) -val decompose_lam_n_assum : int -> constr -> rel_context * constr |