diff options
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 8 |
1 files changed, 4 insertions, 4 deletions
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 |