diff options
Diffstat (limited to 'kernel/term.mli')
| -rw-r--r-- | kernel/term.mli | 36 |
1 files changed, 18 insertions, 18 deletions
diff --git a/kernel/term.mli b/kernel/term.mli index 4d340399d..181d714ed 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -25,14 +25,14 @@ val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr val mkNamedProd : Id.t -> types -> types -> types (** Constructs either [(x:t)c] or [[x=b:t]c] *) -val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types -val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types -val mkNamedProd_or_LetIn : Context.Named.Declaration.t -> types -> types -val mkNamedProd_wo_LetIn : Context.Named.Declaration.t -> types -> types +val mkProd_or_LetIn : Constr.rel_declaration -> types -> types +val mkProd_wo_LetIn : Constr.rel_declaration -> types -> types +val mkNamedProd_or_LetIn : Constr.named_declaration -> types -> types +val mkNamedProd_wo_LetIn : Constr.named_declaration -> types -> types (** Constructs either [[x:t]c] or [[x=b:t]c] *) -val mkLambda_or_LetIn : Context.Rel.Declaration.t -> constr -> constr -val mkNamedLambda_or_LetIn : Context.Named.Declaration.t -> constr -> constr +val mkLambda_or_LetIn : Constr.rel_declaration -> constr -> constr +val mkNamedLambda_or_LetIn : Constr.named_declaration -> constr -> constr (** {5 Other term constructors. } *) @@ -74,8 +74,8 @@ val to_lambda : int -> constr -> constr where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *) val to_prod : int -> constr -> constr -val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr -val it_mkProd_or_LetIn : types -> Context.Rel.t -> types +val it_mkLambda_or_LetIn : constr -> Constr.rel_context -> constr +val it_mkProd_or_LetIn : types -> Constr.rel_context -> types (** In [lambda_applist c args], [c] is supposed to have the form [λΓ.c] with [Γ] without let-in; it returns [c] with the variables @@ -126,29 +126,29 @@ val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr (** Extract the premisses and the conclusion of a term of the form "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *) -val decompose_prod_assum : types -> Context.Rel.t * types +val decompose_prod_assum : types -> Constr.rel_context * types (** Idem with lambda's and let's *) -val decompose_lam_assum : constr -> Context.Rel.t * constr +val decompose_lam_assum : constr -> Constr.rel_context * constr (** Idem but extract the first [n] premisses, counting let-ins. *) -val decompose_prod_n_assum : int -> types -> Context.Rel.t * types +val decompose_prod_n_assum : int -> types -> Constr.rel_context * types (** Idem for lambdas, _not_ counting let-ins *) -val decompose_lam_n_assum : int -> constr -> Context.Rel.t * constr +val decompose_lam_n_assum : int -> constr -> Constr.rel_context * constr (** Idem, counting let-ins *) -val decompose_lam_n_decls : int -> constr -> Context.Rel.t * constr +val decompose_lam_n_decls : int -> constr -> Constr.rel_context * constr (** Return the premisses/parameters of a type/term (let-in included) *) -val prod_assum : types -> Context.Rel.t -val lam_assum : constr -> Context.Rel.t +val prod_assum : types -> Constr.rel_context +val lam_assum : constr -> Constr.rel_context (** Return the first n-th premisses/parameters of a type (let included and counted) *) -val prod_n_assum : int -> types -> Context.Rel.t +val prod_n_assum : int -> types -> Constr.rel_context (** Return the first n-th premisses/parameters of a term (let included but not counted) *) -val lam_n_assum : int -> constr -> Context.Rel.t +val lam_n_assum : int -> constr -> Constr.rel_context (** Remove the premisses/parameters of a type/term *) val strip_prod : types -> types @@ -167,7 +167,7 @@ val strip_lam_assum : constr -> constr Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = Context.Rel.t * Sorts.t +type arity = Constr.rel_context * Sorts.t (** Build an "arity" from its canonical form *) val mkArity : arity -> types |