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 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 4 |
1 files changed, 3 insertions, 1 deletions
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 () |