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

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 97c84858c..8f5d0c96e 100644
--- a/helm/gTopLevel/proofEngine.ml
+++ b/helm/gTopLevel/proofEngine.ml
@@ -575,15 +575,15 @@ let reduction_tactic reduction_function term =
 ;;
 
 let reduction_tactic_in_scratch reduction_function ty term =
- let curi,metasenv,pbo,pty =
+ let metasenv =
   match !proof with
-     None -> assert false
-   | Some (curi,metasenv,bo,ty) -> curi,metasenv,bo,ty
+     None -> []
+   | Some (_,metasenv,_,_) -> metasenv
  in
- let (metano,context,_) =
+ let context =
   match !goal with
-     None -> assert false
-   | Some (metano,(context,ty)) -> metano,context,ty
+     None -> []
+   | Some (_,(context,_)) -> context
  in
   let term' = reduction_function term in
    ProofEngineReduction.replace ~what:term ~with_what:term' ~where:ty