snapshot

[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 be082121ad3ac58720ca946232e7534acfd85e8c..6987937d5e440710782613bf2e084e26425644d3 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPt.ml
+++ b/helm/ocaml/cic_notation/cicNotationPt.ml
@@ -71,6 +71,7 @@ type term =
 
   (* Syntax pattern extensions *)
 
+  | Literal of literal
   | Layout of layout_pattern
   | Magic of magic_term
   | Variable of pattern_variable
@@ -119,3 +120,12 @@ and pattern_variable =
   (* level 2 variables *)
   | FreshVar of string
 
+type argument_pattern =
+  | IdentArg of string
+  | EtaArg of string option * argument_pattern  (* eta abstraction *)
+
+type cic_appl_pattern =
+  | UriPattern of string
+  | ArgPattern of argument_pattern
+  | ApplPattern of cic_appl_pattern list
+