diff options
| -rw-r--r-- | pretyping/evarutil.ml | 13 | ||||
| -rw-r--r-- | proofs/logic.ml | 4 |
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 |