The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello --

I have a plugin that I'm trying to port to 8.5 and I can not figure out how to construct terms with the appropriate universe constraints. Does anyone know of a simple plugin that correctly parses a term passed to a tactic, applies a function to that term, and declares a constant equal the to the resulting term? I think that I have all of the code that reads a term and builds a definition equal to it, but I need to figure out how to get the universe constraints that are constructed during the application.

This is probably extremely naive, but I thought that there would be a function of roughly the type:

val add_constraints : Term.constr -> Evd.evar_map -> Evd.evar_map

that would extend the evar map with the constraints necessary to type check the given term.

If I'm doing this completely wrong, it would be nice to know that as well.

Thank you.

gregory malecha