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') ->
None -> assert false
| Some (uri,metasenv,bo,gty as proof') ->
(* We push the new meta at the end of the list for pretty-printing *)
(* purposes: in this way metas are ordered. *)
let metasenv' = metasenv@[newmeta,context,ty] in
(* We push the new meta at the end of the list for pretty-printing *)
(* purposes: in this way metas are ordered. *)
let metasenv' = metasenv@[newmeta,context,ty] in
(*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
let bo' =
ProofEngineReduction.replace (==) [term] [C.Meta (newmeta,irl)] bo
(*CSC: Bug: se ci sono due term uguali nella prova dovrei bucarne uno solo!!!*)
let bo' =
ProofEngineReduction.replace (==) [term] [C.Meta (newmeta,irl)] bo
- 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