[] -> []
|_ ->
let must = choose_must list_of_must only in
- prerr_endline "123";
let result =
I.execute mqi_handle
(G.query_of_constraints
(Some CGMatchConclusion.universe)
(must,[],[]) (Some only,None,None)) in
- prerr_endline "456";
let uris =
List.map
(function uri,_ ->
not (suffix = ".var") in
let uris = List.filter isvar uris in
(* delete all not "cic:/Coq" uris *)
+ (*
let uris =
(* TODO ristretto per ragioni di efficienza *)
- List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in
+ List.filter (fun _,uri -> Pcre.pmatch ~pat:"^cic:/Coq/" uri) uris in
+ *)
+ (*
+ let uris =
+ List.filter (fun _,uri -> not (Pcre.pmatch ~pat:"^cic:/Coq/ring" uri)) uris in
+ *)
(* concl_cost are the costants in the conclusion of the proof
while hyp_const are the constants in the hypothesis *)
let (_,concl_const) = NewConstraints.constants_of ty in