]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_omdoc/cic2acic.mli
We do not longer generate inner-types and inner-sorts for XML files generated
[helm.git] / helm / ocaml / cic_omdoc / cic2acic.mli
index ff75618f84f2b41413c54e002decde233bf5a0c3..abe61f38769871fb007e1e53c83e686dabfd7dc4 100644 (file)
@@ -57,3 +57,4 @@ val asequent_of_sequent :
     (Cic.id, sort_kind) Hashtbl.t *       (* ids_to_inner_sorts *)
     (Cic.id, Cic.hypothesis) Hashtbl.t    (* ids_to_hypotheses *)
 
+val plain_acic_object_of_cic_object : Cic.obj -> Cic.annobj