• François Bobot's avatar
    session: metas can be added · 3e20cfe5
    François Bobot authored
      - the symbols that appear in the metas are identified in the xml by
        their position in the task:
        - in which declaration
        - in which definition (if that apply otherwise -1)
        - in which constructor(or case in inductive predicate) (if that apply otherwise -1)
        - in which field (if that apply otherwise -1)
      - the md5sum of the prefix of the task that end with the declaration is used to know if the
        symbol have been changed, and if it is obsolete.
      - currently metas that contains obsolete symbol are removed.
gconfig.mli 4.42 KB