From c7d2d6da56d97250ee7ab619ee8c310d91fa912d Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 19 Apr 2002 13:03:44 +0000 Subject: [PATCH] Bug fixed: reduction in the scratch window now works even if there is no proof in progress. --- helm/gTopLevel/proofEngine.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) 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 -- 2.39.2