The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

Also, you may want to look at the code implementing Coq's unify tactic, which is in the file:

https://github.com/coq/coq/blob/741f3fab052b91eaec57f32b639ca722c3d8dc34/tactics/tactics.ml#L5044

In general, when I am wondering "how do I do .... in Coq's OCaml codebase", I recall a tactic or vernacular command doing something similar and find its implementation.

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Tue, May 23, 2017 at 4:16 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

I'd guess you're looking for something like w_unify: https://github.com/coq/coq/blob/trunk/pretyping/unification.mli#L49

On Tue, May 23, 2017 at 1:30 PM Talia Ringer <tringer AT cs.washington.edu> wrote:

Hi all,

I'm writing a Coq plugin that finds patches for small changes in theorems and proofs.

Right now, there is a point in my tool where it would be very useful to query out to unification rather than reinvent the wheel. The unification problems I'm dealing with should be easy enough for Coq to solve most of the time.

Does anyone know how I can call out to unification from a plugin in OCaml? Has anyone done this? I am on Coq 8.5 right now, which may make a difference since I know the unification algorithm and tooling has changed very recently.

Best,

Talia

University of Washington