X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngine.ml;h=97c84858c2ab4bad1210fabaeaf4498659b556d3;hb=a3ea60dba4a46e32ab70a0ebda36367a8186a59f;hp=90d18998111695f18578ddc6ae031f27c89876e0;hpb=7d44fa19cb262a8180a9e48d210311bf0732dbb3;p=helm.git

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 90d189981..97c84858c 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -574,10 +574,31 @@ let reduction_tactic reduction_function term =
       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 =