diff options
| author | Maxime Dénès | 2017-11-28 09:52:18 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-28 09:52:18 +0100 |
| commit | 5a540c372648493575461a298e04b9fa716661ad (patch) | |
| tree | a5c6a9b455b93841dc0960b8b0c1e78865c96b1a /pretyping/pretype_errors.ml | |
| parent | ac006d8c87a7e921ed5a106aeba264bd6c8caa6c (diff) | |
| parent | 3cc45d57f6001d8c377825b9b940bc51fb3a96f7 (diff) | |
Merge PR #6248: [api] Remove aliases of `Evar.t`
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index ce478ac202..7149d62a19 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -7,20 +7,19 @@ (************************************************************************) open Names -open Constr open Environ open EConstr open Type_errors type unification_error = - | OccurCheck of existential_key * constr + | OccurCheck of Evar.t * constr | NotClean of existential * env * constr (* Constr is a variable not in scope *) | NotSameArgSize | NotSameHead | NoCanonicalStructure | ConversionFailed of env * constr * constr (* Non convertible closed terms *) - | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key * env * types * types + | MetaOccurInBody of Evar.t + | InstanceNotSameType of Evar.t * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error | ProblemBeyondCapabilities @@ -39,8 +38,8 @@ type pretype_error = (* Type inference unification *) | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (* Tactic unification *) - | UnifOccurCheck of existential_key * constr - | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option + | UnifOccurCheck of Evar.t * constr + | UnsolvableImplicit of Evar.t * Evd.unsolvability_explanation option | CannotUnify of constr * constr * unification_error option | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr @@ -57,7 +56,7 @@ type pretype_error = | TypingError of type_error | CannotUnifyOccurrences of subterm_unification_error | UnsatisfiableConstraints of - (existential_key * Evar_kinds.t) option * Evar.Set.t option + (Evar.t * Evar_kinds.t) option * Evar.Set.t option exception PretypeError of env * Evd.evar_map * pretype_error |