update in grafite parser

+ parameter notation in record fields

diff --git a/matita/components/grafite_parser/grafiteParser.ml b/matita/components/grafite_parser/grafiteParser.ml
index 929e68e3ccd2fee83030e70911cb39226295cad0..429efbf52b4590e9e19d0e6561ef5e0bae067b26 100644 (file)
--- a/matita/components/grafite_parser/grafiteParser.ml
+++ b/matita/components/grafite_parser/grafiteParser.ml
@@ -481,15 +481,16 @@ EXTEND
       params = LIST0 protected_binder_vars;
        SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ; 
        fields = LIST0 [ 
-         name = IDENT ; 
+         name = IDENT ;
+         params = LIST0 protected_binder_vars; (* FG: params added *)
          coercion = [ 
              SYMBOL ":" -> false,0 
            | SYMBOL ":"; SYMBOL ">" -> true,0
            | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
          ]; 
          ty = term -> 
-           let b,n = coercion in 
-           (name,ty,b,n) 
+           let b,n = coercion in
+           (name, shift_params `Forall params ty, b, n) 
        ] SEP SYMBOL ";"; SYMBOL "}" -> 
         let params =
           List.fold_right

diff --git a/matita/matita/predefined_virtuals.ml b/matita/matita/predefined_virtuals.ml
index 7656dc68c240f516dbf6ade102046239d29e2f8e..548bb9a931f8119b26d53c3a542c4a37919e36d6 100644 (file)
--- a/matita/matita/predefined_virtuals.ml
+++ b/matita/matita/predefined_virtuals.ml
@@ -1574,7 +1574,7 @@ let predefined_classes = [
  ["s"; "σ"; "ς"; "𝕤"; "𝐬"; "𝛔"; "ⓢ"; ] ;
  ["S"; "Σ"; "𝕊"; "𝐒"; "𝚺"; "Ⓢ"; "𝗦"; ] ;
  ["t"; "τ"; "𝕥"; "𝐭"; "𝛕"; "ⓣ"; ] ;
- ["T"; "𝕋"; "𝐓"; "Ⓣ"; "⊥"; ] ;
+ ["T"; "𝕋"; "𝐓"; "Ⓣ"; "Ƭ"; "⊥"; ] ;
  ["u"; "𝕦"; "𝐮"; "ⓤ"; ] ;
  ["U"; "𝕌"; "𝐔"; "Ⓤ"; ] ;
  ["v"; "ν"; "𝕧"; "𝐯"; "𝛖"; "𝛎"; "ⓥ"; "▼"; ] ;