From 0ef1b22756cb35d80cfc47056e0f6f0401c151df Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 8 Jun 2018 15:01:43 +0200 Subject: Add a bit of doc to EConstr.decompose_lam* --- engine/eConstr.mli | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'engine/eConstr.mli') diff --git a/engine/eConstr.mli b/engine/eConstr.mli index b0e834b2e..e9d3e782b 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -182,9 +182,21 @@ val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint val decompose_app : Evd.evar_map -> t -> t * t list +(** Pops lambda abstractions until there are no more, skipping casts. *) val decompose_lam : Evd.evar_map -> t -> (Name.t * t) list * t + +(** Pops lambda abstractions and letins until there are no more, skipping casts. *) val decompose_lam_assum : Evd.evar_map -> t -> rel_context * t + +(** Pops [n] lambda abstractions, and pop letins only if needed to + expose enough lambdas, skipping casts. + + @raise UserError if the term doesn't have enough lambdas. *) val decompose_lam_n_assum : Evd.evar_map -> int -> t -> rel_context * t + +(** Pops [n] lambda abstractions and letins, skipping casts. + + @raise UserError if the term doesn't have enough lambdas/letins. *) val decompose_lam_n_decls : Evd.evar_map -> int -> t -> rel_context * t val compose_lam : (Name.t * t) list -> t -> t -- cgit v1.2.3