256 chars max ==> 1024 chars max (because of Coq)

[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..3d6242e962bb705e72ac7f24d557427827c0f1f9 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
@@ -88,8 +89,9 @@ and layout_pattern =
   | Below of term * term
   | Above of term * term
   | Frac of term * term
+  | Over of term * term
   | Atop of term * term
-(*   | Array of term * literal option * literal option
+(*   | array of term * literal option * literal option
       |+ column separator, row separator +| *)
   | Sqrt of term
   | Root of term * term (* argument, index *)
@@ -119,3 +121,28 @@ 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
+
+type value =
+  | TermValue of term
+  | StringValue of string
+  | NumValue of string
+  | OptValue of value option
+  | ListValue of value list
+
+type value_type =
+  | TermType
+  | StringType
+  | NumType
+  | OptType of value_type
+  | ListType of value_type
+
+type declaration = string * value_type
+