X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationFwd.mli;h=4a5d89f98095c299a05fe9d7ed6c508dbe5ee1a8;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=0cb0a8669454a7658597a6564e7ff3929d3a61c7;hpb=724827ba7e5c1419229382487bed53f7dbb862db;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationFwd.mli b/helm/ocaml/cic_notation/cicNotationFwd.mli
index 0cb0a8669..4a5d89f98 100644
--- a/helm/ocaml/cic_notation/cicNotationFwd.mli
+++ b/helm/ocaml/cic_notation/cicNotationFwd.mli
@@ -28,3 +28,9 @@ val instantiate_level2:
   CicNotationEnv.t -> CicNotationPt.term ->
     CicNotationPt.term
 
+  (** @param env environment from argument_pattern to cic terms
+   * @param pat cic_appl_pattern *)
+val instantiate_appl_pattern:
+  (string * Cic.term) list -> CicNotationPt.cic_appl_pattern ->
+    Cic.term
+