- let ((_, metasenv, _, _), metano) = status in
- let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
- let list_of_must, only = CGMatchConclusion.get_constraints metasenv ey ty in
-match list_of_must with
- [] -> []
-|_ ->
- let must = choose_must list_of_must only in
- let result =
- I.execute mqi_handle
- (G.query_of_constraints
- (Some CGMatchConclusion.universe)
- (must,[],[]) (Some only,None,None)) in
+ let ((_, metasenv, _, _), metano) = status in
+ let (_, ey ,ty) = CicUtil.lookup_meta metano metasenv in
+ let conn =
+ match mqi_handle.MQIConn.pgc with
+ MQIConn.MySQL_C conn -> conn
+ | _ -> assert false in
+ let result = Match_concl.cmatch conn ty in
+ List.iter
+ (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) result;