Small change in the printing of proofs for use by coqide.

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

3 files changed, 3 insertions, 3 deletions

diff --git a/proofs/proof.mli b/proofs/proof.mli
index d0b7e9839d..fcfe1c5c01 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -42,7 +42,7 @@ type proof
 (* In this version: returns the focused goals, a representation of the
    focus stack (the number of goals at each level) and the underlying
    evar_map *)
-val proof : proof -> Goal.goal list * int list * Evd.evar_map
+val proof : proof -> Goal.goal list * (Goal.goal list * Goal.goal list) list * Evd.evar_map
 
 (*** General proof functions ***)
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index d9c62600d4..00e311cc90 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -97,7 +97,7 @@ let list_goto =
    order) *)
 type focus_context = Goal.goal list * Goal.goal list
 
-let focus_context (l,r) = List.length l + List.length r
+let focus_context f = f
 
 (* This (internal) function extracts a sublist between two indices, and
    returns this sublist together with its context:
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index d29ab4f090..d9cc43e504 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -62,7 +62,7 @@ type focus_context
    refined functions to ide-s. This would be better than spawning a
    new nearly identical function everytime. Hence the generic name. *)
 (* In this version: returns the number of goals that are held *)
-val focus_context : focus_context -> int
+val focus_context : focus_context -> Goal.goal list * Goal.goal list
 
 (* [focus i j] focuses a proofview on the goals from index [i] to index [j] 
    (inclusive). (i.e. goals number [i] to [j] become the only goals of the