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 | |
| 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 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 diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index f617df9ee..880f48e5f 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 fa47cc431..244174f65 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 () |