coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Talia Ringer <tringer AT cs.washington.edu>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Calling out to unification from a plugin
Date: Wed, 24 May 2017 02:23:10 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Neutral smtp.mailfrom=e AT x80.org; spf=None smtp.helo=postmaster AT cc-tupan-roaming-a.ensmp.fr
Ironport-phdr: 9a23:foeTABYzC4a1TnFpoAHXAoj/LSx+4OfEezUN459isYplN5qZr8i4bnLW6fgltlLVR4KTs6sC0LuI9f2/ESxYuNDa4S9EKMQNHzY+yuwo3CUYQ/S5QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4VvJ6IwxxfTonZFefldyWd0KV6OhRrx6MO98Zx5/yhMp/4t8tNLXLnncag/UbFXAzMqPnwv6sHsqRfNUxaE6GEGUmURnBpIAgzF4w//U5zsrCb0tfdz1TeDM8HuQr86RTqt76FwSB/1kygHLCI28HvWisNrkq1Wpg+qqgFlzI7VZIGVM+d+fr/YcNgHS2dNQtpdWipcCY6ncYABE/QOMvpZr4nlplsBsx2+BRW3BOjyzjNEn2L60bEm3+gkFwzNwQ4uEM8UsHnMrNv7KrocUee7zKfGzzrNbP1Z1jjh54XTbhAtveuBUa5sfcfLy0QiER7OgFWKqYziOjOYzvoCvnOU7udjSe6jkWknqxt+ojOywssihYzJhoMRylDF8iVy3YI7KsOjSFZhet6vDZpeuDueN4tyXMwiTGZoszsmx70cuJ60ZjMKxJEhyhXCaPKHa5CF7g/nWeueOzt0mm9pdb2lixqv8UWtyffwWtS63VtJtiZIlsfAumoJ2hDP8MSLVOZx8l2g1DuN0Q3Y9/tKLloulaXBLp4s2r4wmYQXsUTEBiL5hFn5gLaKdkU54uin8eLnbqz8pp+bLYB0jwD+MqIhmsCmG+s0KBYBX26A+eS5zL3v50P5QK9Sgv03lKnWrozaKNwGqqO9DAJZyJgv5wuwAju8zdgVnXoKIEhYdB+JjIXlI1TOL+r5Dfe7jVSsijBrx/XeM7L/GZjMIXvOnKv7cbZ68U5cxxI/zcpD6JJMFrEBPPXzV1ftu9zfFx81KhC7w+L6CNpmzY4eQmKOAqqBMKzIq1OI5+QvI/ONZIAPojr9JeIltLbSiioFkFscdOGT3J0YZWrwSuh8IkOWbGDEicxHDm4Rvgs4Q/DtjhuPXSMFNFioWKdp6xkrWNrgCp3MDsCAhb2F3SDzPJBN9HsOJVmIFXrncM2tQfYFc2PBcYdajjUYWO35GMca3ha0uVq/kuI/Iw==
Organization: X80 Heavy Industries

Hi Talia,

Talia Ringer
<tringer AT cs.washington.edu>
writes:

> 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.

It is very common to call unification from plugins, however you should
use Evarconv.the_conv_x .

w_unify in unification.ml is deprecated and may be removed anytime.

You are also strongly encouraged to move to Coq 8.7; in particular, the
new release uses a more strict API for "open" terms (EConstr) which
will really help getting the details about variables fine.

Note that in Coq, substitutions are stored in an "evar map", so you need
to be careful when dealing with open terms.

Best regards,
E.

p.s: Coq's gitter may be a good place to ask more concrete questions.

[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