From e9100d33377eb2bb958ecba6049c6a46f4e9db7f Mon Sep 17 00:00:00 2001
From: barras
Date: Mon, 11 Feb 2002 16:31:44 +0000
Subject: substitution et pattern modulo let

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2466 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/term.mli | 6 ++++++
 1 file changed, 6 insertions(+)

(limited to 'kernel')

diff --git a/kernel/term.mli b/kernel/term.mli
index b676376d3d..00f835e0d5 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -474,6 +474,12 @@ val map_constr : (constr -> constr) -> constr -> constr
 val map_constr_with_binders :
   ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
 
+(* [iter_constr f c] iters [f] on the immediate subterms of [c]; it is
+   not recursive and the order with which subterms are processed is
+   not specified *)
+
+val iter_constr : (constr -> unit) -> constr -> unit
+
 (* [iter_constr_with_binders g f n c] iters [f n] on the immediate
    subterms of [c]; it carries an extra data [n] (typically a lift
    index) which is processed by [g] (which typically add 1 to [n]) at
-- 
cgit v1.2.3