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)
| "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