diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac_classes.ml | 3 | ||||
| -rw-r--r-- | plugins/subtac/subtac_pretyping_F.ml | 8 |
3 files changed, 8 insertions, 5 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 571ec4ef34..f75678c60f 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -210,7 +210,7 @@ open Auto let extend_with_auto_hints l seq gl= let seqref=ref seq in - let f (_, p_a_t) = + let f p_a_t = match p_a_t.code with Res_pf (c,_) | Give_exact c | Res_pf_THEN_trivial_fail (c,_) -> diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index 000ffc6226..c08dd16df5 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -179,9 +179,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p Evarutil.check_evars env Evd.empty !evars termtype; let hook vis gr = let cst = match gr with ConstRef kn -> kn | _ -> assert false in - let inst = Typeclasses.new_instance k pri global (ConstRef cst) in Impargs.declare_manual_implicits false gr ~enriching:false [imps]; - Typeclasses.add_instance inst + Typeclasses.declare_instance pri (not global) (ConstRef cst) in let evm = Subtac_utils.evars_of_term !evars Evd.empty term in let obls, _, constr, typ = Eterm.eterm_obligations env id !evars evm 0 term termtype in diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml index d300a71ccc..d5d427c7a6 100644 --- a/plugins/subtac/subtac_pretyping_F.ml +++ b/plugins/subtac/subtac_pretyping_F.ml @@ -599,8 +599,12 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (pretype_type empty_valcon env evdref lvar c).utj_val in if resolve_classes then - evdref := Typeclasses.resolve_typeclasses ~onlyargs:false - ~split:true ~fail:fail_evar env !evdref; + (try + evdref := Typeclasses.resolve_typeclasses ~onlyargs:true + ~split:true ~fail:true env !evdref; + evdref := Typeclasses.resolve_typeclasses ~onlyargs:false + ~split:true ~fail:false env !evdref + with e -> if fail_evar then raise e else ()); evdref := consider_remaining_unif_problems env !evdref; let c = if expand_evar then nf_evar !evdref c' else c' in if fail_evar then check_evars env Evd.empty !evdref c; |