Mentions légales du service

Skip to content
  • Guillaume Melquiond's avatar
    Move Coq realizations from a .ml file to a driver file. · cc79baa8
    Guillaume Melquiond authored
    Note that the file is still generated at compilation time.
    
    The "realized" meta takes two arguments. The first one is the path+name of
    the theory, the second one is the translation of it for the target prover.
    The meta is supposed to be put into a printer file, so there is no
    ambiguity on the target. The second argument can be left empty if it can be
    inferred from the first one.
    
    Note that the first argument is not really satisfactory, since it is
    redundant with the theory part of the driver. Moreover, its handling is a
    bit crude: it does not take into account rich qualifiers and it does not
    generate proper error messages if it does not match the theory.
    cc79baa8