aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/sign.mli
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/sign.mli')
-rw-r--r--kernel/sign.mli1
1 files changed, 1 insertions, 0 deletions
diff --git a/kernel/sign.mli b/kernel/sign.mli
index bb2e083de..30e1dae28 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -25,6 +25,7 @@ val ids_of_var_context : var_context -> identifier list
val map_var_context : (constr -> constr) -> var_context -> var_context
val mem_var_context : identifier -> var_context -> bool
val fold_var_context : (var_declaration -> 'a -> 'a) -> var_context -> 'a -> 'a
+val fold_var_context_reverse : ('a -> var_declaration -> 'a) -> 'a -> var_context -> 'a
val fold_var_context_both_sides :
('a -> var_declaration -> var_context -> 'a) -> var_context -> 'a -> 'a
val it_var_context_quantifier :