diff options
| author | Emilio Jesus Gallego Arias | 2020-06-30 15:57:33 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-06-30 15:57:33 +0200 |
| commit | 9c9330f2e3a5ff205973881003c5734034b7d0d5 (patch) | |
| tree | ba410bd04083fe3f8bf6a0f70fb4a1fa66663115 /plugins/ltac | |
| parent | bffe3e8dcbb6019b30d32081f0b56eba30bf8be7 (diff) | |
| parent | 6bb0c6df0dd331b8acb78a720eaf076aea5fce47 (diff) | |
Merge PR #12599: Remove the Refiner module
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/rewrite.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 6 |
2 files changed, 5 insertions, 5 deletions
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index f16d0717df..40dea90c00 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1567,7 +1567,7 @@ let assert_replacing id newt tac = let newfail n s = let info = Exninfo.reify () in - Proofview.tclZERO ~info (Refiner.FailError (n, lazy s)) + Proofview.tclZERO ~info (Tacticals.FailError (n, lazy s)) let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = let open Proofview.Notations in @@ -1656,7 +1656,7 @@ let cl_rewrite_clause_strat progress strat clause = (fun (e, info) -> match e with | RewriteFailure e -> tclZEROMSG ~info (str"setoid rewrite failed: " ++ e) - | Refiner.FailError (n, pp) -> + | Tacticals.FailError (n, pp) -> tclFAIL ~info n (str"setoid rewrite failed: " ++ Lazy.force pp) | e -> Proofview.tclZERO ~info e)) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 705a1a62ce..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 @@ -1103,8 +1102,8 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacProgress tac -> Tacticals.New.tclPROGRESS (interp_tactic ist tac) | TacShowHyps tac -> Proofview.V82.tactic begin - tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) - end [@ocaml.warning "-3"] + Tacticals.tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac)) + end | TacAbstract (t,ido) -> let call = LtacMLCall tac in let trace = push_trace(None,call) ist in @@ -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) |