diff options
Diffstat (limited to 'pretyping/typeclasses.ml')
| -rw-r--r-- | pretyping/typeclasses.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 1541e96635..aa2e96c2d7 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -31,7 +31,6 @@ type hint_info = (Pattern.patvar list * Pattern.constr_pattern) hint_info_gen let get_typeclasses_unique_solutions = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"check that typeclasses proof search returns unique solutions" ~key:["Typeclasses";"Unique";"Solutions"] ~value:false @@ -107,9 +106,9 @@ let class_info env sigma c = not_a_class env sigma (EConstr.of_constr (printable_constr_of_global c)) let global_class_of_constr env sigma c = - try let gr, u = Termops.global_of_constr sigma c in + try let gr, u = EConstr.destRef sigma c in GlobRef.Map.find gr !classes, u - with Not_found -> not_a_class env sigma c + with DestKO | Not_found -> not_a_class env sigma c let dest_class_app env sigma c = let cl, args = EConstr.decompose_app sigma c in @@ -125,9 +124,9 @@ let class_of_constr env sigma c = with e when CErrors.noncritical e -> None let is_class_constr sigma c = - try let gr, u = Termops.global_of_constr sigma c in + try let gr, u = EConstr.destRef sigma c in GlobRef.Map.mem gr !classes - with Not_found -> false + with DestKO | Not_found -> false let rec is_class_type evd c = let c, _ = Termops.decompose_app_vect evd c in @@ -140,9 +139,9 @@ let is_class_evar evd evi = is_class_type evd evi.Evd.evar_concl let is_class_constr sigma c = - try let gr, u = Termops.global_of_constr sigma c in + try let gr, u = EConstr.destRef sigma c in GlobRef.Map.mem gr !classes - with Not_found -> false + with DestKO | Not_found -> false let rec is_maybe_class_type evd c = let c, _ = Termops.decompose_app_vect evd c in |