X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationPt.ml;h=d1a54bcf2e3f3e2e8713bc1a54df8102a721d8e1;hb=9f8a383035b272c628c555b728e84caf9229cd57;hp=e9683521ef455a02f33c686523c40aeb5c919171;hpb=9230a8085102cd39258c047949e87001be6ffcf0;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml
index e9683521e..d1a54bcf2 100644
--- a/helm/ocaml/cic_notation/cicNotationPt.ml
+++ b/helm/ocaml/cic_notation/cicNotationPt.ml
@@ -129,16 +129,17 @@ and pattern_variable =
   | FreshVar of string
 
 type argument_pattern =
-  | IdentArg of string
-  | EtaArg of string option * argument_pattern  (* eta abstraction *)
+  | IdentArg of int * string (* eta-depth, name *)
 
 type cic_appl_pattern =
   | UriPattern of string
-  | ArgPattern of argument_pattern
+  | VarPattern of string
   | ApplPattern of cic_appl_pattern list
 
 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