From b7fd585b89ac5e0b7770f52739c33fe179f2eed8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 5 Nov 2016 21:36:40 +0100 Subject: Evarsolve API using EConstr. --- pretyping/pretype_errors.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'pretyping/pretype_errors.ml') diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index f28fb84ba..c14d81505 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -13,14 +13,14 @@ open Environ open Type_errors type unification_error = - | OccurCheck of existential_key * constr - | NotClean of existential * env * constr (* Constr is a variable not in scope *) + | OccurCheck of existential_key * EConstr.constr + | NotClean of EConstr.existential * env * EConstr.constr (* Constr is a variable not in scope *) | NotSameArgSize | NotSameHead | NoCanonicalStructure - | ConversionFailed of env * constr * constr (* Non convertible closed terms *) + | ConversionFailed of env * EConstr.constr * EConstr.constr (* Non convertible closed terms *) | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key * env * types * types + | InstanceNotSameType of existential_key * env * EConstr.types * EConstr.types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error | ProblemBeyondCapabilities -- cgit v1.2.3