]> matita.cs.unibo.it Git - helm.git/commit
update in grafite parser
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 18 Jan 2022 17:50:48 +0000 (18:50 +0100)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Tue, 18 Jan 2022 17:50:48 +0000 (18:50 +0100)
commit55ea9387fd71564c629fe3f47fd9bac59c4befb9
tree041cd9d25c2961aeac37acf7cab664b02ae6750a
parentab63ef8e3b4029307eea9646b099c04a1d499653
update in grafite parser

+ parameter notation in record fields
matita/components/grafite_parser/grafiteParser.ml
matita/matita/predefined_virtuals.ml