diff options
| author | Pierre-Marie Pédrot | 2020-06-26 12:50:46 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-06-29 15:20:35 +0200 |
| commit | d28af587b9848c6155c7eae482591836f0fbc68f (patch) | |
| tree | f485f9cd2c05bd05d2b02c832fe732f1419004e0 /tactics/class_tactics.ml | |
| parent | f34dcb97406611704c93970ea623d6a8587e5ba8 (diff) | |
Move the FailError exception from Refiner to Tacticals.
Diffstat (limited to 'tactics/class_tactics.ml')
| -rw-r--r-- | tactics/class_tactics.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 4156d5f0ee..82ce2234e3 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -1183,7 +1183,7 @@ let resolve_one_typeclass env ?(sigma=Evd.from_env env) gl unique = try Proofview.V82.of_tactic (Search.eauto_tac (modes,st) ~only_classes:true ~depth [hints] ~dep:true) gls - with Refiner.FailError _ -> raise Not_found + with Tacticals.FailError _ -> raise Not_found in let evd = sig_sig gls' in let t' = mkEvar (ev, subst) in |