snapshot (first working implementation of parttern matching from level 2

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

diff --git a/helm/ocaml/cic_notation/cicNotationUtil.mli b/helm/ocaml/cic_notation/cicNotationUtil.mli
index 14cec5826a1017c5fcfac56ecfe408f2cd1ed8bf..b5e242b7fca86f80fdce7a277c080b7100ca5d24 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationUtil.mli
+++ b/helm/ocaml/cic_notation/cicNotationUtil.mli
@@ -25,3 +25,16 @@
 
 val fresh_name: unit -> string
 
+val visit_ast:
+  ?special_k:(CicNotationPt.term -> CicNotationPt.term) ->
+  (CicNotationPt.term -> CicNotationPt.term) ->
+  CicNotationPt.term ->
+    CicNotationPt.term
+
+val visit_layout:
+  (CicNotationPt.term -> CicNotationPt.term) ->
+  CicNotationPt.layout_pattern ->
+    CicNotationPt.layout_pattern
+
+val strip_attributes: CicNotationPt.term -> CicNotationPt.term
+