• Andrei Paskevich's avatar
    store locations in term/formulas, not in labels · f530689a
    Andrei Paskevich authored
    - the new syntax for localisation "labels" in Why is as follows:
    
        goal Toto #"file" line bchar echar#     - after an ident
        #"file" line bchar echar" (A and B)     - before a term/fmla
    
    - the new syntax for buffer relocation is as follows:
    
        ##"file" line char##
    f530689a
pgm_typing.ml 53.5 KB