-
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.
35418b73