diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 6 | ||||
| -rw-r--r-- | pretyping/typeclasses.ml | 4 | ||||
| -rw-r--r-- | pretyping/typeclasses.mli | 2 |
3 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index df1e45d868..19df941b28 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -653,7 +653,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct | IsType -> (pretype_type empty_valcon env evdref lvar c).utj_val in let evd,_ = consider_remaining_unif_problems env !evdref in - let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in + let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:false env (evars_of evd) evd in evdref := evd; nf_evar (evars_of evd) c' @@ -667,7 +667,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let j = pretype empty_tycon env evdref ([],[]) c in let evd,_ = consider_remaining_unif_problems env !evdref in let j = j_nf_evar (evars_of evd) j in - let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:true env (evars_of evd) evd in + let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~fail:true env (evars_of evd) evd in let j = j_nf_evar (evars_of evd) j in check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j @@ -687,7 +687,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct let c = pretype_gen evdref env lvar kind c in let evd,_ = consider_remaining_unif_problems env !evdref in if fail_evar then - let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~all:false env (evars_of evd) evd in + let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env (evars_of evd) evd in let c = Evarutil.nf_isevar evd c in check_evars env Evd.empty evd c; evd, c diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 0450709605..e9a766a92e 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -407,10 +407,10 @@ let has_typeclasses evd = && is_resolvable evi)) evd false -let resolve_typeclasses ?(onlyargs=false) ?(all=true) env sigma evd = +let resolve_typeclasses ?(onlyargs=false) ?(fail=true) env sigma evd = if not (has_typeclasses sigma) then evd else - !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs all + !solve_instanciations_problem env (Evarutil.nf_evar_defs evd) onlyargs fail type substitution = (identifier * constr) list diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index d35ee54140..c6763a4213 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -74,7 +74,7 @@ val bool_out : Dyn.t -> bool val is_resolvable : evar_info -> bool val mark_unresolvable : evar_info -> evar_info -val resolve_typeclasses : ?onlyargs:bool -> ?all:bool -> env -> evar_map -> evar_defs -> evar_defs +val resolve_typeclasses : ?onlyargs:bool -> ?fail:bool -> env -> evar_map -> evar_defs -> evar_defs val solve_instanciation_problem : (env -> evar_defs -> existential_key -> evar_info -> evar_defs * bool) ref val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> evar_defs) ref |