bug #790: better error_not_clean

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

3 files changed, 15 insertions, 13 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 1ccf8f523..9b29f47a6 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -283,7 +283,7 @@ let non_instantiated sigma =
  * false. The problem is that we won't get the right error message.
  *)
 
-let real_clean isevars ev args rhs =
+let real_clean env isevars ev args rhs =
   let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in
   let rec subs k t =
     match kind_of_term t with
@@ -309,7 +309,7 @@ let real_clean isevars ev args rhs =
   in
   let body = subs 0 rhs in
   if not (closed0 body)
-  then error_not_clean empty_env isevars.evars ev body;
+  then error_not_clean env isevars.evars ev body (evar_source ev isevars);
   body
 
 let make_evar_instance_with_rel env =
@@ -377,14 +377,14 @@ let new_isevar isevars env src typ =
  * ?1 would be instantiated by (le y y) but y is not in the scope of ?1
  *)
 
-let evar_define isevars (ev,argsv) rhs =
+let evar_define env isevars (ev,argsv) rhs =
   if occur_evar ev rhs
-  then error_occur_check empty_env (evars_of isevars) ev rhs;
+  then error_occur_check env (evars_of isevars) ev rhs;
   let args = Array.to_list argsv in 
   let evd = ise_map isevars ev in
   (* the bindings to invert *)
   let worklist = make_subst (evar_env evd) args in
-  let body = real_clean isevars ev worklist rhs in
+  let body = real_clean env isevars ev worklist rhs in
   ise_define isevars ev body;
   [ev]
 
@@ -515,11 +515,11 @@ let solve_simple_eqn conv_algo env isevars (pbty,(n1,args1 as ev1),t2) =
 	  solve_refl conv_algo env isevars n1 args1 args2
 	else
 	  if Array.length args1 < Array.length args2 then 
-	    evar_define isevars ev2 (mkEvar ev1)
+	    evar_define env isevars ev2 (mkEvar ev1)
 	  else 
-	    evar_define isevars ev1 t2
+	    evar_define env isevars ev1 t2
     | _ ->
-	evar_define isevars ev1 t2 in
+	evar_define env isevars ev1 t2 in
   let pbs = get_changed_pb isevars lsp in
   List.for_all (fun (pbty,t1,t2) -> conv_algo env isevars pbty t1 t2) pbs
 
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 8b913faa9..a5e1922e0 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -24,7 +24,7 @@ type pretype_error =
   | CantFindCaseType of constr
   (* Unification *)
   | OccurCheck of existential_key * constr
-  | NotClean of existential_key * constr
+  | NotClean of existential_key * constr * hole_kind
   | UnsolvableImplicit of hole_kind
   (* Pretyping *)
   | VarNotFound of identifier
@@ -133,9 +133,10 @@ let error_occur_check env sigma ev c =
   let c = nf_evar sigma c in
   raise (PretypeError (env_ise sigma env, OccurCheck (ev,c)))
 
-let error_not_clean env sigma ev c =
+let error_not_clean env sigma ev c (loc,k) =
   let c = nf_evar sigma c in
-  raise (PretypeError (env_ise sigma env, NotClean (ev,c)))
+  raise_with_loc loc
+    (PretypeError (env_ise sigma env,  NotClean (ev,c,k)))
 
 let error_unsolvable_implicit loc env sigma e =
   raise_with_loc loc (PretypeError (env_ise sigma env, UnsolvableImplicit e))
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 6fd4fc05a..4e98c8a2c 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -25,7 +25,7 @@ type pretype_error =
   | CantFindCaseType of constr
   (* Unification *)
   | OccurCheck of existential_key * constr
-  | NotClean of existential_key * constr
+  | NotClean of existential_key * constr * hole_kind
   | UnsolvableImplicit of hole_kind
   (* Pretyping *)
   | VarNotFound of identifier
@@ -76,7 +76,8 @@ val error_ill_typed_rec_body_loc :
 
 val error_occur_check : env ->  Evd.evar_map -> existential_key -> constr -> 'b
 
-val error_not_clean : env ->  Evd.evar_map -> existential_key -> constr -> 'b
+val error_not_clean :
+  env ->  Evd.evar_map -> existential_key -> constr -> loc * hole_kind -> 'b
 
 val error_unsolvable_implicit : loc -> env -> Evd.evar_map -> hole_kind -> 'b