X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.mli;h=fbd0ea16657c44e86116e2f9bcb08698c1905b91;hb=7f72a2bf9a6f79c58048c594dc390265365face8;hp=cac67cb21c923df9f35a8a84d8f44cb0bb1bdc01;hpb=5530db2f72548a8c579ae5f9868cbd38290eb065;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli
index cac67cb21..fbd0ea166 100644
--- a/helm/ocaml/cic_notation/cicNotationRew.mli
+++ b/helm/ocaml/cic_notation/cicNotationRew.mli
@@ -29,3 +29,15 @@ val ast_of_acic:
     CicNotationPt.term                              (* ast *)
     * (Cic.id, string) Hashtbl.t                    (* id -> uri *)
 
+type interpretation_id
+
+val add_interpretation:
+  string * CicNotationPt.argument_pattern list ->   (* level 2 pattern *)
+  CicNotationPt.cic_appl_pattern ->                 (* level 3 pattern *)
+    interpretation_id
+
+exception Interpretation_not_found
+
+  (** @raise Interpretation_not_found *)
+val remove_interpretation: interpretation_id -> unit
+