[ssr] fix implementation of refine ~first_goes_last

2 files changed, 14 insertions, 14 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index ec9a937f80..0b3bfab366 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -973,7 +973,7 @@ let dependent_apply_error =
  *
  * Refiner.refiner that does not handle metas with a non ground type but works
  * with dependently typed higher order metas. *)
-let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
+let applyn ~with_evars ?beta ?(with_shelve=false) ?(first_goes_last=false) n t gl =
   if with_evars then
     let refine gl =
       let t, ty, args, gl = pf_saturate ?beta ~bi_types:true gl t n in
@@ -985,8 +985,11 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
       pf_partial_solution gl t gs
     in
     Proofview.(V82.of_tactic
-      (tclTHEN (V82.tactic refine)
-        (if with_shelve then shelve_unifiable else tclUNIT ()))) gl
+      (Tacticals.New.tclTHENLIST [
+        V82.tactic refine;
+        (if with_shelve then shelve_unifiable else tclUNIT ());
+        (if first_goes_last then cycle 1 else tclUNIT ())
+        ])) gl
   else
     let t, gl = if n = 0 then t, gl else
       let sigma, si = project gl, sig_it gl in
@@ -1001,21 +1004,17 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl =
           | _ -> assert false
       in loop sigma t [] n in
     pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t));
-    Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t) gl
+    Proofview.(V82.of_tactic
+      (Tacticals.New.tclTHENLIST [
+         V82.tactic (Refiner.refiner ~check:false EConstr.Unsafe.(to_constr t));
+         (if first_goes_last then cycle 1 else tclUNIT ())
+      ])) gl
 
 let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl =
-  let rec mkRels = function 1 -> [] | n -> mkRel n :: mkRels (n-1) in
   let uct = Evd.evar_universe_context (fst oc) in
-  let n, oc = pf_abs_evars_pirrel gl (fst oc, EConstr.Unsafe.to_constr (snd oc)) in
+  let n, oc = pf_abs_evars_pirrel gl (fst oc, EConstr.to_constr ~abort_on_undefined_evars:false (fst oc) (snd oc)) in
   let gl = pf_unsafe_merge_uc uct gl in
-  let oc = if not first_goes_last || n <= 1 then oc else
-    let l, c = decompose_lam oc in
-    if not (List.for_all_i (fun i (_,t) -> Vars.closedn ~-i t) (1-n) l) then oc else
-    compose_lam (let xs,y = List.chop (n-1) l in y @ xs) 
-      (mkApp (compose_lam l c, Array.of_list (mkRel 1 :: mkRels n)))
-  in
-  pp(lazy(str"after: " ++ Printer.pr_constr_env (pf_env gl) (project gl) oc));
-  try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
+  try applyn ~with_evars ~first_goes_last ~with_shelve:true ?beta n (EConstr.of_constr oc) gl
   with e when CErrors.noncritical e -> raise dependent_apply_error
 
 (* We wipe out all the keywords generated by the grammar rules we defined. *)
diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli
index 585db41de0..3049f67f87 100644
--- a/plugins/ssr/ssrcommon.mli
+++ b/plugins/ssr/ssrcommon.mli
@@ -312,6 +312,7 @@ val applyn :
            with_evars:bool ->
            ?beta:bool ->
            ?with_shelve:bool ->
+           ?first_goes_last:bool ->
            int ->
            EConstr.t -> v82tac
 exception NotEnoughProducts