From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 19 Apr 2002 13:03:44 +0000 (+0000)
Subject: Bug fixed: reduction in the scratch window now works even if there is no
X-Git-Tag: V_0_3_0_debian_8~136
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=c7d2d6da56d97250ee7ab619ee8c310d91fa912d

Bug fixed: reduction in the scratch window now works even if there is no
proof in progress.
---

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