None -> assert false
| Some (uri, metasenv, bo, ty) ->
let currentproof =
None -> assert false
| Some (uri, metasenv, bo, ty) ->
let currentproof =
| None,_
| _,None -> assert false
| Some proof', Some goal' ->
let (newproof, newgoals) = tactic ~status:(proof', goal') in
| None,_
| _,None -> assert false
| Some proof', Some goal' ->
let (newproof, newgoals) = tactic ~status:(proof', goal') in
None -> assert false
| Some (uri,metasenv,bo,gty as proof') ->
let newmeta = new_meta proof' in
None -> assert false
| Some (uri,metasenv,bo,gty as proof') ->
let newmeta = new_meta proof' in
- proof := Some (uri,metasenv'',bo',gty) ;
+ set_proof (Some (uri,metasenv'',bo',gty)) ;
(* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
let reduction_tactic_in_scratch reduction_function terms ty =
let metasenv =
(* Reduces [term] using [reduction_function] in the current scratch goal [ty] *)
let reduction_tactic_in_scratch reduction_function terms ty =
let metasenv =
None -> []
| Some (_,metasenv,_,_) -> metasenv
in
None -> []
| Some (_,metasenv,_,_) -> metasenv
in