diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-12 16:00:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-06-12 16:03:39 +0200 |
| commit | 1f772656fa4bb6899ffea84ad5483e9690bbdc08 (patch) | |
| tree | 251fcc193bd523728bbb3e3509c0f4869618dfeb /pretyping/pretype_errors.ml | |
| parent | 59e1618ccda6bbc9c627df93db7aaa3ea5930ccf (diff) | |
Reserve exception "ConversionFailed" in unification for failure of
conversion on closed terms.
This will be useful to discriminate problems involving the "with"
clause and which fails by lack of information or for deeper reasons.
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index cf5b08c58..b0715af73 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -14,15 +14,16 @@ open Type_errors type unification_error = | OccurCheck of existential_key * constr - | NotClean of existential * env * constr + | NotClean of existential * env * constr (* Constr is a variable not in scope *) | NotSameArgSize | NotSameHead | NoCanonicalStructure - | ConversionFailed of env * constr * constr + | ConversionFailed of env * constr * constr (* Non convertible closed terms *) | MetaOccurInBody of existential_key | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error + | ProblemBeyondCapabilities type position = (Id.t * Locus.hyp_location_flag) option |