Skip to content

alternative implementation of mk_evar that keeps naive_solver working

Ralf Jung requested to merge ralf/mk_evar into master

This uses a hack to have side-effects in an ltac that returns a value.

Fixes #115 (closed)

Merge request reports