+ let true_URI =
+ match LibraryObjects.true_URI () with
+ Some uri -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"true\" definition first. Please use the \"default\" command")) in
+ let false_URI =
+ match LibraryObjects.false_URI () with
+ Some uri -> uri
+ | None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default \"false\" definition first. Please use the \"default\" command")) in