• Sylvain Dailler's avatar
    fixes #19 · 35418b73
    Sylvain Dailler authored
    Adding a new tactic apply_with which allows to give an ordered list of
    terms to instantiate variables that are not found by apply. Same for
    rewrite with rewrite_with. These tactics will be merged with apply/rewrite
    when detached are implemented. This needs to be tested extensively.
    Also, print terms with their types in errors.
apply.ml 22.4 KB