From: Ferruccio Guidi Date: Tue, 18 Jan 2022 17:50:48 +0000 (+0100) Subject: update in grafite parser X-Git-Tag: make_still_working~109 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=55ea9387fd71564c629fe3f47fd9bac59c4befb9;p=helm.git 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 929e68e3c..429efbf52 100644 --- 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>; 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 7656dc68c..548bb9a93 100644 --- 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"; "ν"; "𝕧"; "𝐯"; "𝛖"; "𝛎"; "ⓥ"; "▼"; ] ;