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

diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml
index e9683521e..b8fdcfac6 100644
--- a/helm/ocaml/cic_notation/cicNotationPt.ml
+++ b/helm/ocaml/cic_notation/cicNotationPt.ml
@@ -141,4 +141,6 @@ type phrase = (* TODO hackish: replace with TacticAst.statement or similar *)
   | Print of term
   | Notation of term * Gramext.g_assoc option * int option * term
       (* level 1 pattern, associativity, precedence, level 2 pattern *)
+  | Interpretation of (string * argument_pattern list) * cic_appl_pattern
+  | Render of UriManager.uri