From c1b832890049031ee5b3796b926d5f509e3616af Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Sep 2005 14:41:47 +0000
Subject: [PATCH] Assert false (for imbricated theorems) changed to a nice
 error message.

---
 helm/matita/matitaEngine.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 3c54f5a1b..46c83de3f 100644
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -489,8 +489,8 @@ let disambiguate_obj status obj =
     match status.proof_status with
     | No_proof -> Intermediate metasenv
     | Incomplete_proof _
-    | Intermediate _
-    | Proof _ -> assert false
+    | Proof _ -> command_error "imbricated proofs not allowed"
+    | Intermediate _ -> assert false
   in
   let status = { status with proof_status = proof_status } in
   let status = MatitaSync.set_proof_aliases status aliases in
-- 
2.39.2