]> matita.cs.unibo.it Git - helm.git/blobdiff - matita/components/acic_content/termAcicContent.mli
- cic_exportation, cic_acic, acic_content (only parts related to acic)
[helm.git] / matita / components / acic_content / termAcicContent.mli
index bf6ee6a93498efd23714f61cdb00bd7b1a14479e..f7ac8ccc667f5a5e7c326a4343cf2d44c2f4a573 100644 (file)
@@ -51,15 +51,6 @@ val get_all_interpretations: unit -> (interpretation_id * string) list
 val get_active_interpretations: unit -> interpretation_id list
 val set_active_interpretations: interpretation_id list -> unit
 
-  (** {2 acic -> content} *)
-
-val ast_of_acic:
-  output_type:[`Pattern|`Term] ->
-  (Cic.id, CicNotationPt.sort_kind) Hashtbl.t ->    (* id -> sort *)
-  Cic.annterm ->                                    (* acic *)
-    CicNotationPt.term                              (* ast *)
-    * (Cic.id, UriManager.uri) Hashtbl.t            (* id -> uri *)
-
   (** {2 content -> acic} *)
 
   (** @param env environment from argument_pattern to cic terms