X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fcic%2FlibraryObjects.mli;h=bb742f1722481b36ca28b5676ea5e467c19ea6e4;hb=f79567e3b0abcb508c94b66d69d967c4df83082a;hp=0bf8bfea56f165d4d23b5de91e6f6acc67db6958;hpb=2d4775af99f2a2c4a0e7fc7f5cde32a08af4a592;p=helm.git diff --git a/components/cic/libraryObjects.mli b/components/cic/libraryObjects.mli index 0bf8bfea5..bb742f172 100644 --- a/components/cic/libraryObjects.mli +++ b/components/cic/libraryObjects.mli @@ -33,6 +33,10 @@ val is_eq_URI : UriManager.uri -> bool val is_eq_refl_URI : UriManager.uri -> bool val is_eq_ind_URI : UriManager.uri -> bool val is_eq_ind_r_URI : UriManager.uri -> bool +val is_eq_rec_URI : UriManager.uri -> bool +val is_eq_rec_r_URI : UriManager.uri -> bool +val is_eq_rect_URI : UriManager.uri -> bool +val is_eq_rect_r_URI : UriManager.uri -> bool val is_trans_eq_URI : UriManager.uri -> bool val is_sym_eq_URI : UriManager.uri -> bool val is_eq_f_URI : UriManager.uri -> bool @@ -46,6 +50,10 @@ exception NotRecognized of string;; val eq_refl_URI : eq:UriManager.uri -> UriManager.uri val eq_ind_URI : eq:UriManager.uri -> UriManager.uri val eq_ind_r_URI : eq:UriManager.uri -> UriManager.uri +val eq_rec_URI : eq:UriManager.uri -> UriManager.uri +val eq_rec_r_URI : eq:UriManager.uri -> UriManager.uri +val eq_rect_URI : eq:UriManager.uri -> UriManager.uri +val eq_rect_r_URI : eq:UriManager.uri -> UriManager.uri val trans_eq_URI : eq:UriManager.uri -> UriManager.uri val sym_eq_URI : eq:UriManager.uri -> UriManager.uri val eq_f_URI : eq:UriManager.uri -> UriManager.uri @@ -56,3 +64,6 @@ val false_URI : unit -> UriManager.uri option val true_URI : unit -> UriManager.uri option val absurd_URI : unit -> UriManager.uri option +val build_nat : int -> Cic.term +val destroy_nat : Cic.annterm -> int option +