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

[helm.git] / helm / ocaml / cic_notation / cicNotationPt.ml

diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml
index e9683521ef455a02f33c686523c40aeb5c919171..b8fdcfac667e5bf1285d5e130ff270ae9f71b83c 100644 (file)
--- 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