Abstraction de l'implémentation des signatures de Sign en vue intégration du let-in

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@281 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 14 insertions, 1 deletions

diff --git a/kernel/sign.mli b/kernel/sign.mli
index e2ef7d4a1..197028589 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -9,7 +9,7 @@ open Term
 
 (* Signatures of named variables. *)
 
-type 'a signature = identifier list * 'a list
+type 'a signature
 
 val nil_sign : 'a signature
 val add_sign : (identifier * 'a) -> 'a signature -> 'a signature
@@ -23,6 +23,7 @@ val tl_sign : 'a signature -> 'a signature
 val sign_it : (identifier -> 'a -> 'b -> 'b) -> 'a signature -> 'b -> 'b
 val it_sign : ('b -> identifier -> 'a -> 'b) -> 'b -> 'a signature -> 'b
 val concat_sign : 'a signature -> 'a signature -> 'a signature
+
 val ids_of_sign : 'a signature -> identifier list
 val vals_of_sign : 'a signature -> 'a list
 
@@ -64,6 +65,7 @@ val lookup_glob : identifier -> ('b,'a) sign -> (identifier * 'b)
 val lookup_rel : int -> ('b,'a) sign  -> (name * 'a)
 val mem_glob : identifier -> ('b,'a) sign -> bool
 
+val nil_dbsign : 'a db_signature
 val get_globals : ('b,'a) sign -> 'b signature
 val get_rels : ('b,'a) sign -> 'a db_signature
 val dbenv_it : (name -> 'b -> 'c -> 'c) -> ('a,'b) sign -> 'c -> 'c
@@ -73,6 +75,11 @@ val map_var_env : ('c -> 'b) -> ('c,'a) sign -> ('b,'a) sign
 val isnull_rel_env : ('a,'b) sign -> bool
 val uncons_rel_env : ('a,'b) sign -> (name * 'b) * ('a,'b) sign
 val ids_of_env : ('a, 'b) sign -> identifier list
+val number_of_rels : ('b,'a) sign -> int
+
+(*i This is for Cases i*)
+(* raise Not_found if the integer is out of range *)
+val change_name_env: ('a, 'b) sign -> int -> identifier -> ('a, 'b) sign
 
 type ('b,'a) search_result =
   | GLOBNAME of identifier  * 'b
@@ -87,3 +94,9 @@ type var_context = typed_type signature
 
 val unitize_env : 'a assumptions -> unit assumptions
 
+
+
+
+
+
+