• 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
Name
Last commit
Last update
bench Loading commit data...
bin Loading commit data...
comparison Loading commit data...
doc Loading commit data...
drivers Loading commit data...
examples Loading commit data...
lib Loading commit data...
misc Loading commit data...
modules Loading commit data...
plugins Loading commit data...
share Loading commit data...
src Loading commit data...
tests Loading commit data...
theories Loading commit data...
.gitignore Loading commit data...
CHANGES Loading commit data...
DEVELOPER.readme Loading commit data...
INSTALL Loading commit data...
LICENSE Loading commit data...
META.in Loading commit data...
Makefile.in Loading commit data...
OCAML-LICENSE Loading commit data...
README Loading commit data...
ROADMAP Loading commit data...
TODO Loading commit data...
Version Loading commit data...
configure.in Loading commit data...