From f294fe1684e03f63871864def0f82190da087ebe Mon Sep 17 00:00:00 2001
From: Erik Martin-Dorel
Date: Wed, 27 Feb 2019 18:53:11 +0100
Subject: [ssr] under: Fix rewrite goals order when called from under

* "under"-specific behavior:
  the order of goals is kept even if one issues

      Global Set SsrOldRewriteGoalsOrder.

* href: https://github.com/math-comp/math-comp/blob/mathcomp-1.7.0/mathcomp/ssreflect/ssreflect.v
---
 plugins/ssr/ssrequality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index 921dce4689..ff6dd8f75a 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -357,7 +357,7 @@ let pirrel_rewrite ?(under=false) ?(map_redex=id_map_redex) pred rdx rdx_ty new_
   ppdebug(lazy Pp.(str"pirrel_rewrite: proof term: " ++ pr_econstr_env env sigma proof));
   ppdebug(lazy Pp.(str"pirrel_rewrite of type: " ++ pr_econstr_env env sigma proof_ty));
   try refine_with 
-    ~first_goes_last:(not !ssroldreworder) ~with_evars:under (sigma, proof) gl
+    ~first_goes_last:(not !ssroldreworder || under) ~with_evars:under (sigma, proof) gl
   with _ -> 
     (* we generate a msg like: "Unable to find an instance for the variable" *)
     let hd_ty, miss = match EConstr.kind sigma c with
-- 
cgit v1.2.3