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

unnamed proof or leave the possibility of postpone uri choice)

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 ;

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 20863f1a9e366558b694e9483484b2ee279e5509..d9b6219b2d159032f13af762923a069794f7e6c8 100644 (file)
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -38,6 +38,7 @@ let get_current_status_as_xml () =
   match get_proof () with
      None -> assert false
    | Some (uri, metasenv, bo, ty) ->
+      let uri = match uri with Some uri -> uri | None -> assert false in
       let currentproof =
        (*CSC: Wrong: [] is just plainly wrong *)
        Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])

diff --git a/helm/ocaml/tactics/proofEngineTypes.ml b/helm/ocaml/tactics/proofEngineTypes.ml
index d668090e49e2c0f1fd2be733b3ebcbe7b491a55b..3e0a12e4e406a0e689bead48c5da8be38e0b9a54 100644 (file)
--- a/helm/ocaml/tactics/proofEngineTypes.ml
+++ b/helm/ocaml/tactics/proofEngineTypes.ml
@@ -26,7 +26,7 @@
   (**
     current proof (proof uri * metas * (in)complete proof * term to be prooved)
   *)
-type proof = UriManager.uri * Cic.metasenv * Cic.term * Cic.term
+type proof = UriManager.uri option * Cic.metasenv * Cic.term * Cic.term
   (** current goal, integer index *)
 type goal = int
 type status = proof * goal