From 9995a348f823bfcc0b36b105016c0457cc747121 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 24 Jan 2001 16:24:23 +0000
Subject: Ajout global_vars_decl

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

(limited to 'kernel/term.mli')

diff --git a/kernel/term.mli b/kernel/term.mli
index bbd02b6e60..e3f6b44635 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -463,6 +463,10 @@ val subst1_decl : constr -> named_declaration -> named_declaration
 (* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *)
 val global_vars : constr -> identifier list
 
+(* [global_vars_decl d] returns the list of [id]'s occurring as [VAR
+    id] in declaration [d] (type and body if any) *)
+val global_vars_decl : named_declaration -> identifier list
+
 val global_vars_set : constr -> Idset.t
 val replace_vars : (identifier * constr) list -> constr -> constr
 val subst_var : identifier -> constr -> constr
-- 
cgit v1.2.3