From 2bd53620e7f5dea5ddef583ba65ce6c32bbad159 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 20 Jul 2003 15:53:57 +0000 Subject: [PATCH] Cic2acic is now responsible of eta-fixing the objects. --- helm/gTopLevel/gTopLevel.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml index 189f17d3c..ec19107dd 100644 --- a/helm/gTopLevel/gTopLevel.ml +++ b/helm/gTopLevel/gTopLevel.ml @@ -561,9 +561,7 @@ let refresh_proof (output : TermViewer.proof_viewer) = match !ProofEngine.proof with None -> assert false | Some (uri,metasenv,bo,ty) -> - let bo_fixed = Eta_fixing.eta_fix metasenv bo in - let ty_fixed = Eta_fixing.eta_fix metasenv ty in - ProofEngine.proof := Some(uri,metasenv,bo_fixed,ty_fixed); + ProofEngine.proof := Some(uri,metasenv,bo,ty); if List.length metasenv = 0 then begin !qed_set_sensitive true ; @@ -577,7 +575,7 @@ prerr_endline "CSC: ###### REFRESH_PROOF, Hbugs.notify ()" ; end ; (*CSC: Wrong: [] is just plainly wrong *) uri, - (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo_fixed, ty_fixed, [])) + (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])) in ignore (output#load_proof uri currentproof) with -- 2.39.2