(* match main with *)
(* None -> raise Goal_is_not_an_equation *)
(* | Some (m,l) -> *)
- let m, l =
+ let l =
let eq_URI =
- let us = UriManager.string_of_uri (LibraryObjects.eq_URI ()) in
- UriManager.uri_of_string (us ^ "#xpointer(1/1)")
+ match LibraryObjects.eq_URI () with
+ None -> None
+ | Some s ->
+ Some
+ (UriManager.uri_of_string
+ (UriManager.string_of_uri s ^ "#xpointer(1/1)"))
in
- match main with
- | None -> eq_URI, []
- | Some (m, l) when UriManager.eq m eq_URI -> m, l
- | Some (m, l) -> eq_URI, []
+ match eq_URI,main with
+ | Some eq_URI, Some (m, l) when UriManager.eq m eq_URI -> m::l
+ | _,_ -> []
in
Printf.printf "\nSome (m, l): %s, [%s]\n\n"
- (UriManager.string_of_uri m)
- (String.concat "; " (List.map UriManager.string_of_uri l));
+ (UriManager.string_of_uri (List.hd l))
+ (String.concat "; " (List.map UriManager.string_of_uri (List.tl l)));
(* if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *)
let set = signature_of_hypothesis context in
(* Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *)
(* Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *)
let set = close_with_constructors set metasenv context in
(* Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *)
- let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in
+ let set = List.fold_right Constr.UriManagerSet.remove l set in
let uris =
sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
let uris = List.filter nonvar (List.map snd uris) in