From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 24 Jul 2003 14:05:14 +0000 (+0000)
Subject: Exact handled in a better way (no more "NO PROOFS").
X-Git-Tag: LucaOK~34
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=49d5e4fbf175050e4afdf26494eec5231c0eac8d;p=helm.git

Exact handled in a better way (no more "NO PROOFS").
---

diff --git a/helm/ocaml/cic_transformations/content2pres.ml b/helm/ocaml/cic_transformations/content2pres.ml
index cd7bac625..aa10e02ab 100644
--- a/helm/ocaml/cic_transformations/content2pres.ml
+++ b/helm/ocaml/cic_transformations/content2pres.ml
@@ -220,15 +220,19 @@ and proof2pres term2pres p =
       match p.Con.proof_name with
         None -> body
       | Some name ->
-          let ac = 
-        (match concl with
-               None -> P.Mtext([],"NO PROOF!!!")
-             | Some c -> c) in 
           let action = 
-            P.Maction([None,"actiontype","toggle" ;
-                       None,"selection","1"],
-              [(make_concl "proof of" ac);
-                body]) in
+           match concl with
+              None -> body
+(*
+               P.Maction
+                 ([None,"actiontype","toggle" ; None,"selection","1"],
+                  [P.Mtext [] "proof" ; body])
+*)
+            | Some ac ->
+               P.Maction
+                 ([None,"actiontype","toggle" ; None,"selection","1"],
+                  [(make_concl "proof of" ac); body])
+          in
           P.Mtable ([None,"align","baseline 1"; None,"equalrows","false";
               None,"columnalign","left"],
             [P.Mtr ([],[P.Mtd ([],P.Mfenced([],[P.Mtext ([],name)]))]);
@@ -371,16 +375,19 @@ and proof2pres term2pres p =
     else if conclude.Con.conclude_method = "BU_Conversion" then
       assert false
     else if conclude.Con.conclude_method = "Exact" then
-      let conclusion = 
-        (match conclude.Con.conclude_conclusion with 
-           None -> P.Mtext([],"NO Conclusion!!!")
-         | Some c -> term2pres c) in
       let arg = 
         (match conclude.Con.conclude_args with 
            [Con.Term t] -> term2pres t
          | _ -> assert false) in
-      make_row 
-        [arg;P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")] conclusion
+      (match conclude.Con.conclude_conclusion with 
+         None ->
+          P.Mrow []
+           [P.Mtext [None, "mathcolor", "red"] "Consider" ; P.smallskip; arg]
+       | Some c -> let conclusion = term2pres c in
+          make_row 
+            [arg; P.Mspace([None,"width","0.1cm"]);P.Mtext([],"proves")]
+            conclusion
+       )
     else if conclude.Con.conclude_method = "Intros+LetTac" then
       (match conclude.Con.conclude_args with
          [Con.ArgProof p] -> proof2pres p