coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Calling out to unification from a plugin

From: Talia Ringer <tringer AT cs.washington.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Calling out to unification from a plugin
Date: Tue, 23 May 2017 10:25:47 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=tringer AT cs.washington.edu; spf=None smtp.mailfrom=tringer AT cs.washington.edu; spf=None smtp.helo=postmaster AT mail-wm0-f42.google.com
Ironport-phdr: 9a23:YeZPlBKSWOLn9q9+y9mcpTZWNBhigK39O0sv0rFitYgRLP7xwZ3uMQTl6Ol3ixeRBMOAuqwC1rWe8/i5HzdRvtDZ6DFKWacPfiFGoP1VpTBoONSCB0z/IayiRA0BN+MGamVY+WqmO1NeAsf0ag6aiHSz6TkPBke3blItdaz6FYHIksu4yf259YHNbAVUnjq9Zq55IAmroQnLuMQbhYpvJrwxxxbLv3BEf/hayX5yKV+dmxvx5N288IJ//yhVpvks69NOXaLmcqs3SrBVEC4oP2cp6sP1qBLNVxGP5nwSUmUXlhpHHQ3I5wzkU5nyryX3qPNz1DGVMsPqQ780Xy+i77pwRx/zlCgHLT85/3rJhcF2kalWvQiupx17w47TfYGVKP9zdb7TcN8GWWZMWNtaWipcCY2+coQPFfIMM+ZWoYf+ulUAswexCBK2C+/z0DJFnGP60bE43uknDArI3BYgH9ULsHnMstv6LqMSUeGvw6LV0TvDbvVW2Tjj54jSbxsspu2MXahxccrXxkkgCRnFg06Mpoz+JT+U2P4Cs3Ob7+phU+KvhHInqwZ3ojS12Mgjl5TJi5sTx1vZ9it52J44KN+3RUJhfNKoDptduzuZOodoWM8vTH9ktSAnwbMco5G7ZjIFyJE/yh7fdfOHd4+I7wrmVOmLIDd4gGtpeby6hxqu6ESgxOLxWteu3FZFqSpFldbMtnQT2BDJ9seHTf598l+g2TaJyQ/T9vlJLEI7mKbBNpIt3L49moAQvEjdBCP7l1v6gLeTdko+++io7+rnYq/hpp+ZL4J0lhv+MqUomsywH+s4KBMDUHSA+eim2rzs51b5QLVLjv0wnanZrJfaJcIBqqGnHgBVz54v6wyjADe+zNQYgX4HIUpZdxKAlojlIk3BIPTlDfikmFmsizdqx/XePrL7GJnNL37DkK3gfbln8UJcxhAznphj4MdfDahEK/buUGfwssbZB1k3KV+a2eHiXel00oIXEViOBKCUKuuGrUWJ4O0iOcGHf8kKsS39Kv4q+/noy3I1hAlOLuGSwZILZSXgTbxdKEKDbC+0jw==

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

[Coq-Club] Calling out to unification from a plugin, Talia Ringer, 05/23/2017
- Re: [Coq-Club] Calling out to unification from a plugin, Jason Gross, 05/23/2017
  - Re: [Coq-Club] Calling out to unification from a plugin, Abhishek Anand, 05/23/2017
- Re: [Coq-Club] Calling out to unification from a plugin, Emilio Jesús Gallego Arias, 05/24/2017