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 ;
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
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
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
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