X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FgTopLevel.ml;h=0aefe53939e9a1dc91786e24c62480af9101d547;hb=f7b2e35a7bdadb4fdf0e640428e694703ddf67a5;hp=f1710cfce134d60e09f8cdaa3f7d79492402b61e;hpb=70f855932359e26ca89deb11c22f9c9d26154827;p=helm.git

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index f1710cfce..0aefe5393 100644
--- a/helm/gTopLevel/gTopLevel.ml
+++ b/helm/gTopLevel/gTopLevel.ml
@@ -561,6 +561,9 @@ 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);
        if List.length metasenv = 0 then
         begin
          !qed_set_sensitive true ;
@@ -574,7 +577,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, ty, []))
+        (Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo_fixed, ty_fixed, []))
   in
    ignore (output#load_proof uri currentproof)
  with