Use common code in PluginUtils

gmalecha commented 7 years ago

Originally, this code was separate from PluginUtils (https://github.com/gmalecha/coq-plugin-utils) because opam didn't exist and handling dependencies was a pain. With opam, it might be a good idea to consolidate some of the functionality there. In particular:

@yforster noted the the call-ltac function implementation does not work in Coq 8.6 so his PR #31 needs to be back-ported to plugin utils.
A decent amount of the reification code uses code that I stole from the CoqStd module, e.g. constructing Coq values.

@aa755, @mattam82 : Would adding this dependency be problematic for CertiCoq, or is everyone using Opam to install this anyways?

aa755 commented 7 years ago

We use Opam in CertiCoq. Adding this dependency should not be a problem for CertiCoq.

gmalecha commented 7 years ago

Blocking on (https://github.com/gmalecha/coq-plugin-utils/issues/7) for 8.6

gmalecha / template-coq

Use common code in PluginUtils #34