]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/cic2content.mli
first moogle template checkin
[helm.git] / helm / ocaml / cic_omdoc / cic2content.mli
index 16eb5333f721cdc0973b27199bd2c56ffa361440..10ec4b0d1a8fc14e7d66fc1e13dedfd03e05160b 100644 (file)
@@ -28,3 +28,6 @@ val annobj2content :
   ids_to_inner_types:(string, Cic2acic.anntypes) Hashtbl.t ->
   Cic.annobj ->
   Cic.annterm Content.cobj
+
+val map_sequent :
+  Cic.annconjecture -> Cic.annterm Content.conjecture