X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent%2FnotationPt.ml;h=b624c9a8639c6e46a9ba2fef120cbdb6af3d11c8;hb=8f694a82e3291e4a3c2a4f805782846204cf348c;hp=686fcd4ef2ffc1fd3e1bd0b2f7f2e820b001fc0c;hpb=a2412e41cda18a25d780ae631ee02d6ae05c52b1;p=helm.git

diff --git a/matitaB/components/content/notationPt.ml b/matitaB/components/content/notationPt.ml
index 686fcd4ef..b624c9a86 100644
--- a/matitaB/components/content/notationPt.ml
+++ b/matitaB/components/content/notationPt.ml
@@ -51,9 +51,9 @@ type term_attribute =
   ]
 
 type literal =
-  [ `Symbol of string
-  | `Keyword of string
-  | `Number of string
+  [ `Symbol of string * (string option * string option)
+  | `Keyword of string * (string option * string option)
+  | `Number of string * (string option * string option)
   ]
 
 type case_indtype = string * href option
@@ -226,3 +226,11 @@ let binder_prec = 20
 let apply_prec = 70
 let simple_prec = 90
 
+(* sequents *)
+
+type context_entry = 
+    Decl of term
+  | Def of term * term 
+
+type sequent = int * context * term
+and context = (string * context_entry) list