X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=ocaml%2Fpure.ml;h=11cb9af81638ca6f546cd2a7e67ed182a3f9f50c;hb=276d4f75cbe40801f2d9faa82ac82d1c82204e55;hp=7963f8732132a75bab5620326e1c193278af16ff;hpb=5a57b32e5e068d05c1feb7455861bc8d5e4bd05a;p=fireball-separation.git

diff --git a/ocaml/pure.ml b/ocaml/pure.ml
index 7963f87..11cb9af 100644
--- a/ocaml/pure.ml
+++ b/ocaml/pure.ml
@@ -132,6 +132,19 @@ let omega should_explode =
 
 let diverged = (=) B;;
 
+(* Note: maps only variables <= freshno *)
+let env_of_sigma freshno sigma =
+ let rec aux n =
+  if n > freshno then
+   []
+  else
+   let e = aux (n+1) in
+   (try
+    e, lift (-n-1) (snd (List.find (fun (i,_) -> i = n) sigma)),[]
+   with
+    Not_found -> ([], V n, []) ) :: e
+ in aux 0
+
 end
 
 module Scott =