From 04b28b0c95f15fedb2e5eef26cd87b97b4e2120d Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 31 Jul 2014 20:51:48 +0200
Subject: Making the error message about bullets more precise. Suggests in some
 cases the right bullet to use.

---
 proofs/proof.mli | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'proofs/proof.mli')

diff --git a/proofs/proof.mli b/proofs/proof.mli
index be5311fed8..ff1253e7c2 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -115,6 +115,14 @@ val focus : 'a focus_condition -> 'a -> int -> proof -> proof
 
 exception FullyUnfocused
 exception CannotUnfocusThisWay
+
+(* This is raised when trying to focus on non-existing subgoals. It is
+   handled by an error message but one may need to catched it and
+   settle a better error message in some case (suggesting a better
+   bullet for example), see proof_global.ml function Bullet.pop and
+   Bullet.push. *)
+exception NoSuchGoals of int * int
+
 (* Unfocusing command.
    Raises [FullyUnfocused] if the proof is not focused.
    Raises [CannotUnfocusThisWay] if the proof the unfocusing condition
-- 
cgit v1.2.3