From 13ef3c9a4161db85f10c9c5305e44b8ca66f2eaf Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 19 Jan 2016 16:52:04 +0100
Subject: Fixing Not_found on unknown bullet behavior.

---
 proofs/proof_global.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index c32e02344d..46f0db5fe1 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -623,7 +623,10 @@ module Bullet = struct
 	(!current_behavior).name
       end;
       optwrite = begin fun n ->
-	current_behavior := Hashtbl.find behaviors n
+	current_behavior :=
+          try Hashtbl.find behaviors n
+          with Not_found ->
+            Errors.error ("Unknown bullet behavior: \"" ^ n ^ "\".")
       end
     }
 
-- 
cgit v1.2.3