Bug fixed: reduction in the scratch window now works even if there is no

[helm.git] / helm / gTopLevel / proofEngine.ml

diff --git a/helm/gTopLevel/proofEngine.ml b/helm/gTopLevel/proofEngine.ml
index 97c84858c2ab4bad1210fabaeaf4498659b556d3..8f5d0c96e9ef749811d7370a33fc3be52984811c 100644 (file)
--- 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