aboutsummaryrefslogtreecommitdiff
path: root/engine/eConstr.mli
diff options
context:
space:
mode:
Diffstat (limited to 'engine/eConstr.mli')
-rw-r--r--engine/eConstr.mli2
1 files changed, 2 insertions, 0 deletions
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index f897448557..e27eecc24f 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -180,6 +180,8 @@ val destProj : Evd.evar_map -> t -> Projection.t * t
val destFix : Evd.evar_map -> t -> (t, t) pfixpoint
val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint
+val destRef : Evd.evar_map -> t -> GlobRef.t * EInstance.t
+
val decompose_app : Evd.evar_map -> t -> t * t list
(** Pops lambda abstractions until there are no more, skipping casts. *)