snapshot (first version with working pattern matching both 3->2 and 2->1)

[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 b8fdcfac667e5bf1285d5e130ff270ae9f71b83c..d1a54bcf2e3f3e2e8713bc1a54df8102a721d8e1 100644 (file)
--- 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 *)