* 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

4 files changed, 14 insertions, 21 deletions

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
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index b7e1900b12..05d7857c4e 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -27,15 +27,6 @@ open Tacticals
 open Ind_tables
 
 (* boolean equality *)
-(* 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)
-    | (_, []) -> failwith "context_chop"
-  in chop_aux [] (k,ctx)
 
 let quick_chop n l = 
   let rec kick_last = function
@@ -561,9 +552,9 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
                         | Ind (i1,i2) -> 
                             if(string_of_label (label i1) = "eq")
                             then (
-                              tclTHENSEQ (do_replace_bl ind gls (!avoid)
+                              tclTHENSEQ ((do_replace_bl ind gls (!avoid)
                                                       nparrec (ca.(2))
-                                                      (ca.(1))) gls
+                              (ca.(1)))@[Auto.default_auto]) gls
                             )
                             else 
                               (error "Failure while solving Boolean->Leibniz.")
diff --git a/toplevel/command.ml b/toplevel/command.ml
index b5c9cb59bd..44e1b2d941 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -318,16 +318,6 @@ let declare_eq_scheme sp =
 
 (* decidability of eq *)
 
-(* 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) 
-    | (_, []) -> failwith "context_chop" 
-  in chop_aux [] (k,ctx)
-
 
 let (inBoolLeib,outBoolLeib) =
   declare_object {(default_object "BOOLLIEB") with