changed proofStatus so that uri component is optional (useful to start an

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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index e70946564a53b64b1d3b754b0e3b854429210993..1726725c15370b146e42439def72b6b34c23c655 100644 (file)
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -468,6 +468,7 @@ let qed () =
  match ProofEngine.get_proof () with
     None -> assert false
   | Some (uri,[],bo,ty) ->
+     let uri = match uri with Some uri -> uri | _ -> assert false in
      if
       CicReduction.are_convertible []
        (CicTypeChecker.type_of_aux' [] [] bo) ty
@@ -565,8 +566,9 @@ let refresh_proof (output : TermViewer.proof_viewer) =
        else
         Hbugs.notify () ;
        (*CSC: Wrong: [] is just plainly wrong *)
-       uri,
-        (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
+        let uri = match uri with Some uri -> uri | _ -> assert false in
+        (uri,
+         Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, []))
   in
    ignore (output#load_proof uri currentproof)
  with
@@ -691,7 +693,7 @@ let load_unfinished_proof () =
         match CicParser.obj_of_xml proof_file_type (Some proof_file) with
            Cic.CurrentProof (_,metasenv,bo,ty,_) ->
             typecheck_loaded_proof metasenv bo ty ;
-            ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+            ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty));
             refresh_proof output ;
             set_proof_engine_goal
              (match metasenv with
@@ -1512,7 +1514,7 @@ let new_proof () =
    let metasenv,expr = !get_metasenv_and_term () in
     let _  = CicTypeChecker.type_of_aux' metasenv [] expr in
      ProofEngine.set_proof
-      (Some (!get_uri (), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr)) ;
+      (Some (Some (!get_uri ()), (1,[],expr)::metasenv, Cic.Meta (1,[]), expr));
      set_proof_engine_goal (Some 1) ;
      refresh_goals notebook ;
      refresh_proof output ;
@@ -1600,7 +1602,7 @@ let open_ () =
        | Cic.Variable _
        | Cic.InductiveDefinition _ -> raise NotADefinition
      in
-      ProofEngine.set_proof (Some (uri, metasenv, bo, ty)) ;
+      ProofEngine.set_proof (Some (Some uri, metasenv, bo, ty)) ;
       set_proof_engine_goal None ;
       refresh_goals notebook ;
       refresh_proof output ;