diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-11 12:37:44 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-01-11 22:05:14 +0100 |
| commit | 9519878ce3a8e9290a4d7902b1a1dc807252aabb (patch) | |
| tree | d975544edfd9db1e60a133718be76e62aee414ae | |
| parent | 157bf9b96a49b052d12aa646ccb5018750a0b02e (diff) | |
Avoiding a redundant information in unification error message.
| -rw-r--r-- | toplevel/himsg.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 8a9282d1b..b45c8873b 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -260,10 +260,10 @@ let explain_generalization env sigma (name,var) j = str "it has type" ++ spc () ++ pt ++ spc () ++ str "which should be Set, Prop or Type." -let explain_unification_error env sigma p1 p2 = function +let rec explain_unification_error env sigma p1 p2 = function | None -> mt() | Some e -> - let rec aux = function + let rec aux p1 p2 = function | OccurCheck (evk,rhs) -> let rhs = Evarutil.nf_evar sigma rhs in [str "cannot define " ++ quote (pr_existential_key sigma evk) ++ @@ -309,9 +309,9 @@ let explain_unification_error env sigma p1 p2 = function let u = Evarutil.nf_evar sigma u in (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++ str " == " ++ pr_lconstr_env env sigma u) - :: aux e + :: aux t u e in - match aux e with + match aux p1 p2 e with | [] -> mt () | l -> spc () ++ str "(" ++ prlist_with_sep pr_semicolon (fun x -> x) l ++ str ")" |