From 6f9511d66cbca602302d7854b5699e02eb1b026a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 13 Dec 1999 00:05:40 +0000
Subject: Poursuite intégration du Cases

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@242 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/environ.ml  | 14 ++++++++++++++
 kernel/environ.mli |  1 +
 2 files changed, 15 insertions(+)

(limited to 'kernel')

diff --git a/kernel/environ.ml b/kernel/environ.ml
index 5ac91dc00d..eaa87b5be2 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -55,6 +55,20 @@ let change_hyps f env =
   let (ENVIRON(g,r)) = env.env_context in
   { env with env_context = ENVIRON (f g, r) }
 
+(* == functions to deal with names in contexts (previously in cases.ml) == *)
+
+(* If cur=(Rel j) then 
+ * if env = ENVIRON(sign,[na_h:Th]...[na_j:Tj]...[na_1:T1])
+ * then it yields ENVIRON(sign,[na_h:Th]...[Name id:Tj]...[na_1:T1])
+ *)
+let change_name_rel env j id =
+  let ENVIRON(sign,db) = context env in
+  (match list_chop (j-1) db with
+       db1,((_,ty)::db2) ->
+	 {env with env_context = ENVIRON(sign,db1@(Name id,ty)::db2)}
+     | _ -> assert false)
+(****)
+
 let push_rel idrel env =
   { env with env_context = add_rel idrel env.env_context }
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index cfcdf2d36c..ffb5861e1b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -27,6 +27,7 @@ val var_context : env -> var_context
 val push_var : identifier * typed_type -> env -> env
 val change_hyps : 
   (typed_type signature -> typed_type signature) -> env -> env
+val change_name_rel : env -> int -> identifier -> env
 
 val push_rel : name * typed_type -> env -> env
 
-- 
cgit v1.2.3