unification: evar_define checks the free variables are bound in the evar context

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

2 files changed, 12 insertions, 5 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 23f5a74c80..aed6ed9d64 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -285,7 +285,7 @@ let non_instantiated sigma =
  * false. The problem is that we won't get the right error message.
  *)
 
-let real_clean env isevars ev args rhs =
+let real_clean env isevars ev evi args rhs =
   let evd = ref isevars in
   let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in
   let rec subs k t =
@@ -302,7 +302,14 @@ let real_clean env isevars ev args rhs =
 	    else do_restrict_hyps evd ev args'
 	  else
 	    mkEvar (ev,args')
-      | Var _ -> (try List.assoc t subst with Not_found -> t)
+      | Var id ->
+          (try List.assoc t subst
+           with Not_found ->
+             if List.exists (fun (id',_,_) -> id=id') evi.evar_hyps
+             then t
+             else
+               error_not_clean env (evars_of !evd) ev rhs
+                 (evar_source ev !evd))
       | _ -> map_constr_with_binders succ subs k t
   in
   let body = subs 0 rhs in
@@ -335,7 +342,7 @@ let evar_define env (ev,argsv) rhs isevars =
   let evi = Evd.map (evars_of isevars) ev in
   (* the bindings to invert *)
   let worklist = make_subst (evar_env evi) args in
-  let (isevars',body) = real_clean env isevars ev worklist rhs in
+  let (isevars',body) = real_clean env isevars ev evi worklist rhs in
   if occur_meta body then error "Meta cannot occur in evar body"
   else
    let isevars'' = Evd.evar_define ev body isevars' in
diff --git a/proofs/logic.ml b/proofs/logic.ml
index ab5b426339..74a1cf7626 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -50,9 +50,9 @@ let catchable_exception = function
   | Util.UserError _ | TypeError _ | RefinerError _
   (* unification errors *)
   | PretypeError(_,(CannotUnify _|CannotGeneralize _|NoOccurrenceFound _|
-      CannotUnifyBindingType _))
+      CannotUnifyBindingType _|NotClean _))
   | Stdpp.Exc_located(_,PretypeError(_,(CannotUnify _|CannotGeneralize _|
-          NoOccurrenceFound _ | CannotUnifyBindingType _)))
+          NoOccurrenceFound _ | CannotUnifyBindingType _|NotClean _)))
   | Stdpp.Exc_located(_,(Util.UserError _ | TypeError _ | RefinerError _ |
     Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _))) -> true
   | _ -> false