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 /plugins/ltac/tacinterp.ml | |
| parent | f34dcb97406611704c93970ea623d6a8587e5ba8 (diff) | |
Move the FailError exception from Refiner to Tacticals.
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index d65c2f0de9..fdebe14a23 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -22,7 +22,6 @@ open Util open Names open Nameops open Libnames -open Refiner open Tacmach.New open Tactic_debug open Constrexpr @@ -1442,6 +1441,7 @@ and interp_match_success ist { Tactic_matching.subst ; context ; terms ; lhs } = if the left-hand side fails. *) and interp_match_successes lz ist s = let general = + let open Tacticals in let break (e, info) = match e with | FailError (0, _) -> None | FailError (n, s) -> Some (FailError (pred n, s), info) |