No description, website, or topics provided.
Coq
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
src
test-suite
.gitignore
LICENSE
Makefile
README

README

An example of Coq plugin that provides a tactic that generalize the
vm_compute tactic, such that it is possible to use it when existential
variables appear in the goal. 

It also makes it possible to recover some kind of opacity by
abstracting over some definitions that appear in the goal (instances
of these definitions that appear through computations are going to be
expanded, though).

For instance, 
\[
evm blacklist [plus] 
\]

in the goal 

\[
5 * 4 + ?3 
\]

reduces to 

\[
20 + ?3
\]


INSTALL
=================

make 
make install


USAGE
=================

- [evm_compute] perform computation using the vm_compute strategy, even if there are evars in the goal.

- [evm_compute blacklist l] performs computation without unfolding the terms in [l] that appears in the current conclusion (but those that appear through reduction are unfolded). [l] is a list in OCaml syntax (bracketed, semi-colon separated).