X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent%2FnotationPt.ml;fp=matitaB%2Fcomponents%2Fcontent%2FnotationPt.ml;h=4804208f0657e6a8c54397ac1e7e0591355159da;hb=c81b0e8dbfe80e2350e9322afa8316f39f98c3b3;hp=b624c9a8639c6e46a9ba2fef120cbdb6af3d11c8;hpb=935c8d1b73726bb49b99e5c2dbebdea0d617fa1a;p=helm.git

diff --git a/matitaB/components/content/notationPt.ml b/matitaB/components/content/notationPt.ml
index b624c9a86..4804208f0 100644
--- a/matitaB/components/content/notationPt.ml
+++ b/matitaB/components/content/notationPt.ml
@@ -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