From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 21 Nov 2016 12:13:05 +0100 Subject: Reductionops now return EConstrs. --- engine/termops.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'engine/termops.mli') diff --git a/engine/termops.mli b/engine/termops.mli index 426b5f34d..1699d600e 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -130,6 +130,7 @@ val occur_term : Evd.evar_map -> EConstr.t -> EConstr.t -> bool (** Synonymous o (* Substitution of metavariables *) type meta_value_map = (metavariable * constr) list val subst_meta : meta_value_map -> constr -> constr +val isMetaOf : Evd.evar_map -> metavariable -> EConstr.constr -> bool (** Type assignment for metavariables *) type meta_type_map = (metavariable * types) list -- cgit v1.2.3