unnamed proof or leave the possibility of postpone uri choice)
match ProofEngine.get_proof () with
None -> assert false
| Some (uri,[],bo,ty) ->
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
if
CicReduction.are_convertible []
(CicTypeChecker.type_of_aux' [] [] bo) ty
else
Hbugs.notify () ;
(*CSC: Wrong: [] is just plainly wrong *)
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
in
ignore (output#load_proof uri currentproof)
with
match CicParser.obj_of_xml proof_file_type (Some proof_file) with
Cic.CurrentProof (_,metasenv,bo,ty,_) ->
typecheck_loaded_proof metasenv bo ty ;
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
refresh_proof output ;
set_proof_engine_goal
(match metasenv with
let metasenv,expr = !get_metasenv_and_term () in
let _ = CicTypeChecker.type_of_aux' metasenv [] expr in
ProofEngine.set_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 ;
set_proof_engine_goal (Some 1) ;
refresh_goals notebook ;
refresh_proof output ;
| Cic.Variable _
| Cic.InductiveDefinition _ -> raise NotADefinition
in
| 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 ;
set_proof_engine_goal None ;
refresh_goals notebook ;
refresh_proof output ;
match get_proof () with
None -> assert false
| Some (uri, metasenv, bo, ty) ->
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,[])
let currentproof =
(*CSC: Wrong: [] is just plainly wrong *)
Cic.CurrentProof (UriManager.name_of_uri uri,metasenv,bo,ty,[])
(**
current proof (proof uri * metas * (in)complete proof * term to be prooved)
*)
(**
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
(** current goal, integer index *)
type goal = int
type status = proof * goal