snapshot (first version with [apparently] working mappings between level

[helm.git] / helm / ocaml / cic_notation / cicNotationRew.mli

diff --git a/helm/ocaml/cic_notation/cicNotationRew.mli b/helm/ocaml/cic_notation/cicNotationRew.mli
index cac67cb21c923df9f35a8a84d8f44cb0bb1bdc01..fbd0ea16657c44e86116e2f9bcb08698c1905b91 100644 (file)
--- 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
+