From 7730ab45cb810e7ea0dfa804321b339c822ee87a Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Thu, 15 Sep 2005 09:12:59 +0000 Subject: [PATCH] bugfix: default "false" used to set the _true_ uri ... --- helm/ocaml/cic/libraryObjects.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/helm/ocaml/cic/libraryObjects.ml b/helm/ocaml/cic/libraryObjects.ml index 6a1e8a122..967318721 100644 --- a/helm/ocaml/cic/libraryObjects.ml +++ b/helm/ocaml/cic/libraryObjects.ml @@ -52,7 +52,7 @@ let insert_unique e extract l = e :: l' let set_default what l = - match what,l with + 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) @@ -60,7 +60,7 @@ let set_default what l = | "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 + false_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 -- 2.39.2