added the support for the "Locate Inductive Principles" query

[helm.git] / helm / gTopLevel / gTopLevel.ml

diff --git a/helm/gTopLevel/gTopLevel.ml b/helm/gTopLevel/gTopLevel.ml
index 189f17d3ce5288329e50b66b9d85042b4efccb5f..65f381859e299bea48c0c669ec5bd76665214bf6 100644 (file)
--- 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
@@ -1918,7 +1916,7 @@ let completeSearchPattern () =
    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
+    MQG.query_of_constraints (Some CGSearchPattern.universe) must' only
    in
    let results = MQI.execute mqi_handle query in 
     show_query_results results