X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FlibraryObjects.mli;h=3ca7e7292dcf0a9bc0bd461206ed2e8c876117d5;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=859b4e732daf302b55d945e955afb4d152696ed5;hpb=b8ac0d11d5cd4083838a3848fce68683a518b54a;p=helm.git diff --git a/helm/ocaml/cic/libraryObjects.mli b/helm/ocaml/cic/libraryObjects.mli index 859b4e732..3ca7e7292 100644 --- a/helm/ocaml/cic/libraryObjects.mli +++ b/helm/ocaml/cic/libraryObjects.mli @@ -23,12 +23,13 @@ * http://helm.cs.unibo.it/ *) -(*CSC: how can we choose between the two libraries? *) -val eq_URI : UriManager.uri +val set_default : string -> UriManager.uri list -> unit + +val eq_URI : unit -> UriManager.uri val is_eq_URI : UriManager.uri -> bool -exception Not_recognized;; +exception NotRecognized;; val eq_ind_URI : eq:UriManager.uri -> UriManager.uri val eq_ind_r_URI : eq:UriManager.uri -> UriManager.uri @@ -36,6 +37,6 @@ val trans_eq_URI : eq:UriManager.uri -> UriManager.uri val sym_eq_URI : eq:UriManager.uri -> UriManager.uri -val false_URI : UriManager.uri -val true_URI : UriManager.uri -val absurd_URI : UriManager.uri +val false_URI : unit -> UriManager.uri +val true_URI : unit -> UriManager.uri +val absurd_URI : unit -> UriManager.uri