diff options
| -rw-r--r-- | pretyping/evarutil.ml | 16 | ||||
| -rw-r--r-- | pretyping/pretype_errors.ml | 7 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 5 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 45 |
4 files changed, 40 insertions, 33 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 diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index cd2c4b145..0aff2840e 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -314,40 +314,45 @@ let explain_occur_check ctx ev rhs = str"Occur check failed: tried to define " ++ str id ++ str" with term" ++ brk(1,1) ++ pt -let explain_not_clean ctx ev t = - let ctx = make_all_name_different ctx in - let c = mkRel (Intset.choose (free_rels t)) in - let id = Evd.string_of_existential ev in - let var = prterm_env ctx c in - str"Tried to define " ++ str id ++ - str" with a term using variable " ++ var ++ spc () ++ - str"which is not in its scope." - -let explain_unsolvable_implicit env = function - | QuestionMark -> str "Cannot infer a term for this placeholder" +let explain_hole_kind env = function + | QuestionMark -> str "a term for this placeholder" | CasesType -> - str "Cannot infer the type of this pattern-matching problem" + str "the type of this pattern-matching problem" | BinderType (Name id) -> - str "Cannot infer a type for " ++ Nameops.pr_id id + str "a type for " ++ Nameops.pr_id id | BinderType Anonymous -> - str "Cannot infer a type for this anonymous binder" + str "a type for this anonymous binder" | ImplicitArg (c,n) -> if !Options.v7 then - str "Cannot infer the " ++ pr_ord n ++ + str "the " ++ pr_ord n ++ str " implicit argument of " ++ Nametab.pr_global_env Idset.empty c else let imps = Impargs.implicits_of_global c in let id = Impargs.name_of_implicit (List.nth imps (n-1)) in - str "Unable to infer an instance for the implicit parameter " ++ + str "an instance for the implicit parameter " ++ pr_id id ++ spc () ++ str "of" ++ spc () ++ Nametab.pr_global_env Idset.empty c | InternalHole -> - str "Cannot infer a term for an internal placeholder" + str "a term for an internal placeholder" | TomatchTypeParameter (tyi,n) -> - str "Cannot infer the " ++ pr_ord n ++ + str "the " ++ pr_ord n ++ str " argument of the inductive type (" ++ pr_inductive env tyi ++ str ") of this term" +let explain_not_clean ctx ev t k = + let ctx = make_all_name_different ctx in + let c = mkRel (Intset.choose (free_rels t)) in + let id = Evd.string_of_existential ev in + let var = prterm_env ctx c in + str"Tried to define " ++ explain_hole_kind ctx k ++ + str" (" ++ str id ++ str ")" ++ spc() ++ + str"with a term using variable " ++ var ++ spc () ++ + str"which is not in its scope." + +let explain_unsolvable_implicit env k = + str "Cannot infer " ++ explain_hole_kind env k + + let explain_var_not_found ctx id = str "The variable" ++ spc () ++ str (string_of_id id) ++ spc () ++ str "was not found" ++ @@ -412,8 +417,8 @@ let explain_pretype_error ctx err = explain_cant_find_case_type ctx c | OccurCheck (n,c) -> explain_occur_check ctx n c - | NotClean (n,c) -> - explain_not_clean ctx n c + | NotClean (n,c,k) -> + explain_not_clean ctx n c k | UnsolvableImplicit k -> explain_unsolvable_implicit ctx k | VarNotFound id -> |