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

diff --git a/matitaB/components/content/notationPt.ml b/matitaB/components/content/notationPt.ml
index 686fcd4ef..7cdb86c80 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
@@ -62,7 +62,7 @@ type 'term capture_variable = 'term * 'term option
 
 (** To be increased each time the term type below changes, used for "safe"
  * marshalling *)
-let magic = 7
+let magic = 8
 
 type term =
   (* CIC AST *)
@@ -101,8 +101,9 @@ type term =
   | NCic of NCic.term
 
   (* Syntax pattern extensions *)
-
-  | Literal of literal
+  (* string option = optional name of an Ast.Symbol occurring in the level 2
+   * term, which is associated to this literal *)
+  | Literal of (string option * literal)
   | Layout of layout_pattern
 
   | Magic of magic_term
@@ -193,6 +194,12 @@ type 'term obj =
   | Record of 'term capture_variable list * string * 'term * (string * 'term * bool * int) list
       (** left parameters, name, type, fields *)
 
+let name_of_obj = function
+  | Theorem (_,n,_,_,_) | Record (_,n,_,_)
+  | Inductive (_,(n,_,_,_)::_) -> n
+  | _ -> (* empty inductive block *) assert false
+;;
+ 
 let map_variable f (t,u) = f t, HExtlib.map_option f u ;;
 
 let map_pattern f = function
@@ -226,3 +233,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