+(**** TABLES ****)
+
+(* eq, sym_eq, trans_eq, eq_ind, eq_ind_R *)
+let eq_URIs_ref =
+ ref [HelmLibraryObjects.Logic.eq_URI,
+ HelmLibraryObjects.Logic.sym_eq_URI,
+ HelmLibraryObjects.Logic.trans_eq_URI,
+ HelmLibraryObjects.Logic.eq_ind_URI,
+ HelmLibraryObjects.Logic.eq_ind_r_URI];;
+
+let true_URIs_ref = ref [HelmLibraryObjects.Logic.true_URI]
+let false_URIs_ref = ref [HelmLibraryObjects.Logic.false_URI]
+let absurd_URIs_ref = ref [HelmLibraryObjects.Logic.absurd_URI]
+
+
+(**** SET_DEFAULT ****)
+
+exception NotRecognized;;
+
+(* insert an element in front of the list, removing from the list all the
+ previous elements with the same key associated *)
+let insert_unique e extract l =
+ let uri = extract e in
+ let l' =
+ List.filter (fun x -> let uri' = extract x in not (UriManager.eq uri uri')) l
+ in
+ e :: l'
+
+let set_default what l =
+ match what,l with
+ "equality",[eq_URI;sym_eq_URI;trans_eq_URI;eq_ind_URI;eq_ind_r_URI] ->
+ eq_URIs_ref :=
+ insert_unique (eq_URI,sym_eq_URI,trans_eq_URI,eq_ind_URI,eq_ind_r_URI)
+ (fun x,_,_,_,_ -> x) !eq_URIs_ref
+ | "true",[true_URI] ->
+ true_URIs_ref := insert_unique true_URI (fun x -> x) !true_URIs_ref
+ | "false",[false_URI] ->
+ true_URIs_ref := insert_unique false_URI (fun x -> x) !false_URIs_ref
+ | "absurd",[absurd_URI] ->
+ absurd_URIs_ref := insert_unique absurd_URI (fun x -> x) !absurd_URIs_ref
+ | _,_ -> raise NotRecognized
+
+(**** LOOKUP FUNCTIONS ****)
+
+let eq_URI () = let eq,_,_,_,_ = List.hd !eq_URIs_ref in eq