]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/cic/unshare.mli
parameter sintax added to axiom statement
[helm.git] / helm / software / components / cic / unshare.mli
index 5582abcbf31517f50ccb96adc035d965786de714..0dffb532e7a1c56672b23fdcd66c67bdaca239f2 100644 (file)
@@ -23,4 +23,5 @@
  * http://cs.unibo.it/helm/.
  *)
 
-val unshare : Cic.term -> Cic.term
+val unshare : ?fresh_univs:bool -> Cic.term -> Cic.term
+val fresh_types: Cic.obj -> Cic.obj