From d9dc86a6f7194c2e7ea704c95495955ca4f4b08d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Nov 2000 10:26:35 +0000
Subject: Ajout map_constr_with_full_binders et strong pour Simpl

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

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index f909b90da8..d4dbd8ce17 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -631,6 +631,16 @@ val map_constr_with_named_binders :
 val map_constr_with_binders_left_to_right :
   ('a -> 'a) -> ('a -> constr -> constr) -> 'a -> constr -> constr
 
+(* [map_constr_with_named_binders g f l c] maps [f l] on the immediate
+   subterms of [c]; it carries an extra data [l] (typically a name
+   list) which is processed by [g na] (which typically cons [na] to
+   [l]) at each binder traversal (with name [na]); it is not recursive
+   and the order with which subterms are processed is not specified *)
+
+val map_constr_with_full_binders :
+  (rel_declaration -> 'a -> 'a) -> ('a -> constr -> constr) ->
+      'a -> constr -> constr
+
 (* [compare_constr f c1 c2] compare [c1] and [c2] using [f] to compare
    the immediate subterms of [c1] of [c2] if needed; Cast's, binders
    name and Cases annotations are not taken into account *)
-- 
cgit v1.2.3