cicDischarge: new module for discharging the explicit variables occurring in a

[helm.git] / helm / software / components / cic / libraryObjects.mli

diff --git a/helm/software/components/cic/libraryObjects.mli b/helm/software/components/cic/libraryObjects.mli
index f0d8e4631baa309212b73ab7be9b49f927b41484..b4e19dff80452402f04c92609563d4195c630a58 100644 (file)
--- a/helm/software/components/cic/libraryObjects.mli
+++ b/helm/software/components/cic/libraryObjects.mli
@@ -24,8 +24,10 @@
  *)
 
 val set_default : string -> UriManager.uri list -> unit
-val reset_defaults : unit -> unit 
 
+val reset_defaults : unit -> unit 
+val push: unit -> unit
+val pop: unit -> unit
 
 val eq_URI : unit -> UriManager.uri option
 
@@ -64,3 +66,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
+