From ca993b9e7765ac58f70740818758457c9367b0da Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 11 Nov 2016 00:29:02 +0100 Subject: Making judgment type generic over the type of inner constrs. This allows to factorize code and prevents the unnecessary use of back and forth conversions between the various types of terms. Note that functions from typing may now raise errors as PretypeError rather than TypeError, because they call the proper wrapper. I think that they were wrongly calling the kernel because of an overlook of open modules. --- proofs/refine.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs/refine.mli') diff --git a/proofs/refine.mli b/proofs/refine.mli index 3d140f036..4158e446c 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -36,7 +36,7 @@ val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic (** {7 Helper functions} *) val with_type : Environ.env -> Evd.evar_map -> - Term.constr -> Term.types -> Evd.evar_map * Term.constr + Term.constr -> Term.types -> Evd.evar_map * EConstr.constr (** [with_type env sigma c t] ensures that [c] is of type [t] inserting a coercion if needed. *) -- cgit v1.2.3