Reverted commit r13893 about propagation of more informative

unification failure messages (it is not fully usable and was not
intended to be committed now, sorry for the noise).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13895 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 42 deletions

diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index f86d6d271..6af1f9d56 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -153,46 +153,16 @@ let explain_generalization env (name,var) j =
   str "it has type" ++ spc () ++ pt ++
   spc () ++ str "which should be Set, Prop or Type."
 
-let explain_unification_error env p1 p2 = function
-  | None -> mt()
-  | Some e ->
-    match e with
-    | OccurCheck (evk,rhs) ->
-        spc () ++ str "(cannot define " ++ quote (pr_existential_key evk) ++
-	strbrk " with term " ++ pr_lconstr_env env rhs ++
-        strbrk "that would depend on itself)"
-    | NotClean (evk,c) ->
-        spc () ++ str "(cannot instantiate " ++ quote (pr_existential_key evk)
-        ++ strbrk " because " ++ pr_lconstr_env env c ++
-	strbrk " is out of scope)"
-    | NotSameArgSize | NotSameHead | NoCanonicalStructure ->
-        (* Error speaks from itself *) mt ()
-    | ConversionFailed (env,t1,t2) ->
-        if t1 <> p1 || t2 <> p2 then
-          spc () ++ str "(cannot unify " ++ pr_lconstr_env env t1 ++
-	  strbrk " and " ++ pr_lconstr_env env t2 ++ str ")"
-	else mt ()
-    | MetaOccurInBody evk ->
-        spc () ++ str "(instance for " ++ quote (pr_existential_key evk) ++
-	strbrk " refers to a metavariable - please report your example)"
-    | InstanceNotSameType evk ->
-        spc () ++ str "(unable to find a well-typed instantiation for " ++
-	quote (pr_existential_key evk) ++ str ")"
-
-
-let explain_actual_type env sigma j t reason =
+let explain_actual_type env sigma j pt =
   let j = j_nf_betaiotaevar sigma j in
-  let t = Reductionops.nf_betaiota sigma t in
+  let pt = Reductionops.nf_betaiota sigma pt in
   let pe = pr_ne_context_of (str "In environment") env in
   let (pc,pct) = pr_ljudge_env env j in
-  let pt = pr_lconstr_env env t in
-  let ppreason = explain_unification_error env j.uj_type t reason in
+  let pt = pr_lconstr_env env pt in
   pe ++
-  hov 0 (
   str "The term" ++ brk(1,1) ++ pc ++ spc () ++
-  str "has type" ++ brk(1,1) ++ pct ++ spc () ++
-  str "while it is expected to have type" ++ brk(1,1) ++ pt ++
-  ppreason ++ str ".")
+  str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++
+  str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str "."
 
 let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl =
   let randl = jv_nf_betaiotaevar sigma randl in
@@ -450,14 +420,13 @@ let explain_wrong_case_info env ind ci =
     str "was given to a pattern-matching expression on the inductive type" ++
     spc () ++ pc ++ str "."
 
-let explain_cannot_unify env sigma m n e =
+let explain_cannot_unify env sigma m n =
   let m = nf_evar sigma m in
   let n = nf_evar sigma n in
   let pm = pr_lconstr_env env m in
   let pn = pr_lconstr_env env n in
-  let ppreason = explain_unification_error env m n e in
   str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++
-  str "with" ++ brk(1,1) ++ pn ++ ppreason ++ str "."
+  str "with" ++ brk(1,1) ++ pn ++ str "."
 
 let explain_cannot_unify_local env sigma m n subn =
   let pm = pr_lconstr_env env m in
@@ -525,7 +494,7 @@ let explain_type_error env sigma err =
   | Generalization (nvar, c) ->
       explain_generalization env nvar c
   | ActualType (j, pt) ->
-      explain_actual_type env sigma j pt None
+      explain_actual_type env sigma j pt
   | CantApplyBadType (t, rator, randl) ->
       explain_cant_apply_bad_type env sigma t rator randl
   | CantApplyNonFunctional (rator, randl) ->
@@ -542,13 +511,13 @@ let explain_pretype_error env sigma err =
   let env = make_all_name_different env in
   match err with
   | CantFindCaseType c -> explain_cant_find_case_type env sigma c
-  | ActualTypeNotCoercible (j,t,e) -> explain_actual_type env sigma j t (Some e)
-  | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs
+  | OccurCheck (n,c) -> explain_occur_check env sigma n c
+  | NotClean (n,c,k) -> explain_not_clean env sigma n c k
   | UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env evi k exp
   | VarNotFound id -> explain_var_not_found env id
   | UnexpectedType (actual,expect) -> explain_unexpected_type env sigma actual expect
   | NotProduct c -> explain_not_product env sigma c
-  | CannotUnify (m,n,e) -> explain_cannot_unify env sigma m n e
+  | CannotUnify (m,n) -> explain_cannot_unify env sigma m n
   | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn
   | CannotGeneralize ty -> explain_refiner_cannot_generalize env ty
   | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id