]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/content_pres/acic2Procedural.ml
procedural: buggy ast renderer fixed
[helm.git] / helm / software / components / content_pres / acic2Procedural.ml
index 18ded2e7969579acd0fb94707f00a6ce1afc8278..9b8dbf06383143c7759c9b7f06bb1c95df6ec83a 100644 (file)
@@ -236,7 +236,7 @@ let mk_obj st = function
       let text = Printf.sprintf "tactics: %u" count in
       P.Theorem (s, t, text) :: ast @ [P.Qed ""]
    | _                                                               ->
-      [P.Note "not a theorem"]
+      failwith "not a theorem"
 
 (* interface functions ******************************************************)