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

1 files changed, 10 insertions, 0 deletions

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 *)