diff options
| -rw-r--r-- | tactics/class_tactics.ml4 | 5 | ||||
| -rw-r--r-- | toplevel/classes.ml | 1 |
2 files changed, 5 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 9457403cc..a353a4222 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -450,7 +450,10 @@ let select_evars evs evm = let resolve_all_evars debug m env p oevd do_split fail = let oevm = Evd.evars_of oevd in let split = if do_split then split_evars (Evd.evars_of (Evd.undefined_evars oevd)) else [Intset.empty] in - let p = if do_split then fun comp ev evi -> Intset.mem ev comp && p ev evi else fun _ -> p in + let p = if do_split then + fun comp ev evi -> (Intset.mem ev comp || not (Evd.mem oevm ev)) && p ev evi + else fun _ -> p + in let rec aux n p evd = if has_undefined p oevm evd then if n > 0 then diff --git a/toplevel/classes.ml b/toplevel/classes.ml index bac85345b..1d22c3e57 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -281,6 +281,7 @@ let new_class id par ar sup props = let subs = List.map (fun ((loc, id), b, _) -> b) props in (* Instantiate evars and check all are resolved *) let isevars,_ = Evarconv.consider_remaining_unif_problems env_props !isevars in + let isevars = Typeclasses.resolve_typeclasses env_props isevars in let sigma = Evd.evars_of isevars in let ctx_params = Evarutil.nf_named_context_evar sigma ctx_params in let ctx_props = Evarutil.nf_named_context_evar sigma ctx_props in |