coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Get Universe Constraints for constr in plugin

From: Enrico Tassi <enrico.tassi AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Get Universe Constraints for constr in plugin
Date: Tue, 26 May 2015 17:48:56 +0200

On Mon, May 25, 2015 at 11:30:45PM -0400, Gregory Malecha wrote:
> val add_constraints : Term.constr -> Evd.evar_map -> Evd.evar_map

You can use Typing.e_type_of for that.

Best,
--
Enrico Tassi

[Coq-Club] Get Universe Constraints for constr in plugin, Gregory Malecha, 05/26/2015
- Re: [Coq-Club] Get Universe Constraints for constr in plugin, Enrico Tassi, 05/26/2015