Backport PR #12857: [ssr] when porting v8.2 code no backtracking poin…

…t has to be added
coq · Sep 7, 2020 · 180fa5c · 180fa5c
2 parents 1f39281 + bd702a4
commit 180fa5c
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 2 deletions.
diff --git 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
@@ -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))

diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.out b/test-suite/output/ssr_error_multiple_intro_after_case.out
@@ -0,0 +1,3 @@
+File "stdin", line 3, characters 0-11:
+Error: x already used
+
diff --git a/test-suite/output/ssr_error_multiple_intro_after_case.v b/test-suite/output/ssr_error_multiple_intro_after_case.v
@@ -0,0 +1,3 @@
+Require Import ssreflect.
+Goal forall p : nat * nat , True.
+case => x x.