From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Mon, 5 Sep 2005 14:41:47 +0000 (+0000)
Subject: Assert false (for imbricated theorems) changed to a nice error message.
X-Git-Tag: V_0_1_2_1~103
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=c1b832890049031ee5b3796b926d5f509e3616af;p=helm.git

Assert false (for imbricated theorems) changed to a nice error message.
---

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