From a4e02939c27240159946dd037d85db4cf6af2ef1 Mon Sep 17 00:00:00 2001
From: vsiles
Date: Mon, 17 Mar 2008 14:34:34 +0000
Subject: * Factorizing code : context_chop was used in several files (even as
 chop_context) so I moved it to termops.ml * Fixing a little bug in the
 Boolean to Leibniz transition in automatic boolean   declaration

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10686 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/termops.ml  | 10 ++++++++++
 pretyping/termops.mli |  2 ++
 2 files changed, 12 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index e52d7c82aa..01104a8156 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -1064,3 +1064,13 @@ let on_judgment f j = { uj_val = f j.uj_val; uj_type = f j.uj_type }
 let on_judgment_value f j = { j with uj_val = f j.uj_val }
 let on_judgment_type f j = { j with uj_type = f j.uj_type }
 
+(* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k 
+     variables *)
+let context_chop k ctx =
+  let rec chop_aux acc = function
+    | (0, l2) -> (List.rev acc, l2)
+    | (n, ((_,Some _,_ as h)::t)) -> chop_aux (h::acc) (n, t)
+    | (n, (h::t)) -> chop_aux (h::acc) (pred n, t)
+    | (_, []) -> anomaly "context_chop"
+  in chop_aux [] (k,ctx)
+
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index f215d4e9ae..64edcd2e39 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -186,6 +186,8 @@ val ids_of_named_context : named_context -> identifier list
 val ids_of_context : env -> identifier list
 val names_of_rel_context : env -> names_context
 
+val context_chop : int -> rel_context -> (rel_context*rel_context)
+
 (* Set of local names *)
 val vars_of_env: env -> Idset.t
 val add_vname : Idset.t -> name -> Idset.t
-- 
cgit v1.2.3