X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FtacticChaser.ml;h=cb700f776c5debbdfb6bbd716339b2b472ddd4a3;hb=cbac948d507d74a558ba7f11ce10bc252b1ba8ba;hp=2d1b0dcfd14833a5cebde6d5598b9046bfe7c6b6;hpb=31851952e1cc2db59168c5fd6f6093d9bc37ea86;p=helm.git diff --git a/helm/ocaml/tactics/tacticChaser.ml b/helm/ocaml/tactics/tacticChaser.ml index 2d1b0dcfd..cb700f776 100644 --- a/helm/ocaml/tactics/tacticChaser.ml +++ b/helm/ocaml/tactics/tacticChaser.ml @@ -33,6 +33,8 @@ (* *) (*****************************************************************************) +(* $Id$ *) + module MQI = MQueryInterpreter module MQIC = MQIConn module I = MQueryInterpreter @@ -125,11 +127,7 @@ let matchConclusion2 mqi_handle ?(output_html = (fun _ -> ())) ~choose_must() st (* List.iter (fun (n,u) -> prerr_endline ((string_of_int n) ^ " " ^u)) uris; *) (* delete all .var uris *) - let isvar (_,s) = - let len = String.length s in - let suffix = String.sub s (len-4) 4 in - not (suffix = ".var") in - let uris = List.filter isvar uris in + let uris = List.filter UriManager.is_var uris in (* delete all not "cic:/Coq" uris *) (* let uris =