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

diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml
index b8fdcfac6..d1a54bcf2 100644
--- a/helm/ocaml/cic_notation/cicNotationPt.ml
+++ b/helm/ocaml/cic_notation/cicNotationPt.ml
@@ -129,12 +129,11 @@ 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 *)