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 6987937d5e440710782613bf2e084e26425644d3..3d6242e962bb705e72ac7f24d557427827c0f1f9 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPt.ml
+++ b/helm/ocaml/cic_notation/cicNotationPt.ml
@@ -89,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 *)
@@ -129,3 +130,19 @@ type cic_appl_pattern =
   | 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
+