X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FlibraryObjects.ml;h=967318721736a1e1d3a081f165ce63b6608c86e3;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=6a1e8a122c0c42fb81977d7911061c83099cec5b;hpb=a9af753c66a80cb4f50f32e63272f3830cba306c;p=helm.git

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