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

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 0aefe5393..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
@@ -1915,7 +1913,7 @@ let completeSearchPattern () =
  let outputhtml = ((rendering_window ())#outputhtml : GHtml.xmhtml) in
   try
    let metasenv,expr = inputt#get_metasenv_and_term ~context:[] ~metasenv:[] in
-   let must = MQueryLevels2.get_constraints expr in
+   let must = CGSearchPattern.get_constraints expr in
    let must',only = refine_constraints must in
    let query =
     MQG.query_of_constraints (Some MQGU.universe_for_search_pattern) must' only
@@ -2042,10 +2040,10 @@ let choose_must list_of_must only =
      in
       ignore
        (List.map
-         (function (uri,position) ->
+         (function (position, uri) ->
            let n =
             clist#append 
-             [uri; if position then "MainConclusion" else "Conclusion"]
+             [uri; MQGUtil.text_of_position position]
            in
             clist#set_row ~selectable:false n
          ) must
@@ -2074,10 +2072,10 @@ let choose_must list_of_must only =
   in
    ignore
     (List.map
-      (function (uri,position) ->
+      (function (position, uri) ->
         let n =
          clist#append 
-          [uri; if position then "MainConclusion" else "Conclusion"]
+          [uri; MQGUtil.text_of_position position]
         in
          clist#set_row ~selectable:true n
       ) only