From 3f41c704aa09301df18cfc90f72a3895e169d74c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 27 Oct 2006 21:50:17 +0000
Subject: Ajout fold_rel_declaration et fold_named_declaration

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

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index b392d54525..49d4d231b5 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -646,6 +646,9 @@ type rel_declaration = name * constr option * types
 let map_named_declaration f (id, v, ty) = (id, option_map f v, f ty)
 let map_rel_declaration = map_named_declaration
 
+let fold_named_declaration f (_, v, ty) a = f ty (option_fold_right f v a)
+let fold_rel_declaration = fold_named_declaration
+
 (****************************************************************************)
 (*              Functions for dealing with constr terms                     *)
 (****************************************************************************)
-- 
cgit v1.2.3