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

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 3c54f5a1b6730510751e2e96a88d331c38b163fc..46c83de3fcd19002d83efd4c3e2fcc4049b677e7 100644 (file)
--- 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