goal := Some (metano,(context',ty'))
;;
+let reduction_tactic_in_scratch reduction_function ty term =
+ let curi,metasenv,pbo,pty =
+ match !proof with
+ None -> assert false
+ | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
+ in
+ let (metano,context,_) =
+ match !goal with
+ None -> assert false
+ | Some (metano,(context,ty)) -> metano,context,ty
+ in
+ let term' = reduction_function term in
+ ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty
+;;
+
let whd = reduction_tactic CicReduction.whd;;
let reduce = reduction_tactic ProofEngineReduction.reduce;;
let simpl = reduction_tactic ProofEngineReduction.simpl;;
+let whd_in_scratch = reduction_tactic_in_scratch CicReduction.whd;;
+let reduce_in_scratch =
+ reduction_tactic_in_scratch ProofEngineReduction.reduce;;
+let simpl_in_scratch =
+ reduction_tactic_in_scratch ProofEngineReduction.simpl;;
+
(* It is just the opposite of whd. The code should probably be merged. *)
let fold term =
let curi,metasenv,pbo,pty =