* Abst removed from the DTD

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 26c0b2e65c427c16f9001a57db91c40d4b73c4fd..4a8b0a382486a2e082811488e26a28f228b441df 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -744,6 +744,14 @@ let save rendering_window () =
              "/public/sacerdot/currentproof</h1>")
 ;;
 
+(* Used to typecheck the loaded proofs *)
+let typecheck_loaded_proof metasenv bo ty =
+ let module T = CicTypeChecker in
+  (*CSC: bisogna controllare anche il metasenv!!! *)
+  ignore (T.type_of_aux' metasenv [] ty) ;
+  ignore (T.type_of_aux' metasenv [] bo)
+;;
+
 let load rendering_window () =
  let outputhtml = (rendering_window#outputhtml : GHtml.xmhtml) in
  let output = (rendering_window#output : GMathView.math_view) in
@@ -752,6 +760,7 @@ let load rendering_window () =
    let uri = UriManager.uri_of_string "cic:/dummy.con" in
     match CicParser.obj_of_xml "/public/sacerdot/currentproof" uri with
        Cic.CurrentProof (_,metasenv,bo,ty) ->
+        typecheck_loaded_proof metasenv bo ty ;
         ProofEngine.proof :=
          Some (uri, metasenv, bo, ty) ;
         ProofEngine.goal :=