diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarutil.ml | 3 | ||||
| -rw-r--r-- | pretyping/pretype_errors.ml | 6 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 4 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 15 |
4 files changed, 8 insertions, 20 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 1f256b3bd..e8d79703a 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1004,7 +1004,8 @@ let check_evars env initial_sigma evd c = assert (Evd.mem sigma evk); if not (Evd.mem initial_sigma evk) then let (loc,k) = evar_source evk evd in - error_unsolvable_implicit loc env sigma k + let evi = nf_evar_info sigma (Evd.find sigma evk) in + error_unsolvable_implicit loc env sigma evi k | _ -> iter_constr proc_rec c in proc_rec c diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index ad4e06a55..420e0ef9b 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -25,7 +25,7 @@ type pretype_error = (* Unification *) | OccurCheck of existential_key * constr | NotClean of existential_key * constr * Evd.hole_kind - | UnsolvableImplicit of Evd.hole_kind + | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind | CannotUnify of constr * constr | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr @@ -152,8 +152,8 @@ let error_not_clean env sigma ev c (loc,k) = 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)) +let error_unsolvable_implicit loc env sigma evi e = + raise_with_loc loc (PretypeError (env_ise sigma env, UnsolvableImplicit (evi, e))) let error_cannot_unify env sigma (m,n) = raise (PretypeError (env_ise sigma env,CannotUnify (m,n))) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 3a2a2f7f4..c949462c1 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -27,7 +27,7 @@ type pretype_error = (* Unification *) | OccurCheck of existential_key * constr | NotClean of existential_key * constr * Evd.hole_kind - | UnsolvableImplicit of Evd.hole_kind + | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind | CannotUnify of constr * constr | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr @@ -93,7 +93,7 @@ val error_not_clean : env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b val error_unsolvable_implicit : - loc -> env -> Evd.evar_map -> Evd.hole_kind -> 'b + loc -> env -> Evd.evar_map -> Evd.evar_info -> Evd.hole_kind -> 'b val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5b4e8e7cf..db492c026 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -695,14 +695,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct let ise_pretype_gen fail_evar sigma env lvar kind c = let evdref = ref (Evd.create_evar_defs sigma) in let c = pretype_gen evdref env lvar kind c in -(* let evd,_ = consider_remaining_unif_problems env !evdref in *) -(* let evd = nf_evar_defs evd in *) -(* let c = nf_evar (evars_of evd) c in *) -(* let evd = undefined_evars evd in *) -(* let evd = Typeclasses.resolve_typeclasses env sigma evd in *) -(* let c = nf_evar (evars_of evd) c in *) let evd,_ = consider_remaining_unif_problems env !evdref in - if fail_evar then check_evars env (Evd.evars_of evd) evd c; + if fail_evar then check_evars env Evd.empty evd c; evd, c (** Entry points of the high-level type synthesis algorithm *) @@ -721,13 +715,6 @@ module Pretyping_F (Coercion : Coercion.S) = struct let understand_tcc_evars evdref env kind c = pretype_gen evdref env ([],[]) kind c -(* let c = pretype_gen evdref env ([],[]) kind c in *) -(* evdref := nf_evar_defs !evdref; *) -(* let c = nf_evar (evars_of !evdref) c in *) -(* let evd = undefined_evars !evdref in *) -(* let evd = Typeclasses.resolve_typeclasses env (evars_of evd) !evdref in *) -(* evdref := evd; *) -(* nf_evar (evars_of evd) c *) let understand_tcc sigma env ?expected_type:exptyp c = let evd, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in |