From af686af3cf333d2d138e5e3e485fd7228b30ab85 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Wed, 19 Aug 2020 13:57:49 +0200
Subject: [ssr] when porting v8.2 code no backtracking point has to be added

Amends c1b1afe76e1655cc3275bdf4215f0ab690efc3cc
---
 plugins/ssr/ssrcommon.ml   | 2 +-
 plugins/ssr/ssrequality.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index d7996a722a..d859fe51ab 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1047,7 +1047,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc =
   let uct = Evd.evar_universe_context (fst oc) in
   let n, oc = abs_evars_pirrel env sigma (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in
   Proofview.Unsafe.tclEVARS (Evd.set_universe_context sigma uct) <*>
-  Proofview.tclOR (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc))
+  Proofview.tclORELSE (applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc))
     (fun _ -> Proofview.tclZERO dependent_apply_error)
   end
 
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index da623703a2..38b26d06b9 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -465,7 +465,7 @@ let rwcltac ?under ?map_redex cl rdx dir sr =
       Tactics.apply_type ~typecheck:true cl'' [rdx; EConstr.it_mkLambda_or_LetIn r3 dc], Tacticals.New.tclTHENLIST (itacs @ rwtacs), sigma0
   in
   let cvtac' =
-    Proofview.tclOR cvtac begin function
+    Proofview.tclORELSE cvtac begin function
     | (PRtype_error e, _) ->
       let error = Option.cata (fun (env, sigma, te) ->
           Pp.(fnl () ++ str "Type error was: " ++ Himsg.explain_pretype_error env sigma te))
-- 
cgit v1.2.3