diff options
| author | Hugo Herbelin | 2016-06-12 16:00:23 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-12 16:03:39 +0200 |
| commit | 1f772656fa4bb6899ffea84ad5483e9690bbdc08 (patch) | |
| tree | 251fcc193bd523728bbb3e3509c0f4869618dfeb | |
| 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.
| -rw-r--r-- | pretyping/pretype_errors.ml | 5 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 1 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 4 |
3 files changed, 7 insertions, 3 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index cf5b08c58f..b0715af734 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 diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index f617df9ee7..880f48e5f9 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -24,6 +24,7 @@ type unification_error = | 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 diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index fa47cc4311..244174f651 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -65,7 +65,7 @@ let rec contract3' env a b c = function let (env',t1,t2) = contract2 env' t1 t2 in contract3 env a b c, ConversionFailed (env',t1,t2) | NotSameArgSize | NotSameHead | NoCanonicalStructure - | MetaOccurInBody _ | InstanceNotSameType _ + | MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities | UnifUnivInconsistency _ as x -> contract3 env a b c, x | CannotSolveConstraint ((pb,env',t,u),x) -> let env',t,u = contract2 env' t u in @@ -310,6 +310,8 @@ let rec explain_unification_error env sigma p1 p2 = function (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++ str " == " ++ pr_lconstr_env env sigma u) :: aux t u e + | ProblemBeyondCapabilities -> + [] in match aux p1 p2 e with | [] -> mt () |