diff options
| author | barras | 2004-07-13 14:16:53 +0000 |
|---|---|---|
| committer | barras | 2004-07-13 14:16:53 +0000 |
| commit | a60e2ea37b953dbe76b2cf92e7fa06fcc5cc0c35 (patch) | |
| tree | 339c5793ca39635cca86fe3b2c0b0c35319d95c8 /pretyping/evarutil.ml | |
| parent | 49c842d98c3d32016a279f97497876c79cba9880 (diff) | |
bug #790: better error_not_clean
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5896 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 1ccf8f5230..9b29f47a65 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 |