From d69e4f55757c9066b0ae600d14ef89de3c8eb07d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Wed, 8 Nov 2017 10:20:08 +0100
Subject: ssr: fill_occ_pattern: return valid ustate even if no match (fix
 #6106)

---
 plugins/ssr/ssrcommon.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'plugins/ssr')

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 1f2d02093..f7e0a5d93 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -1159,6 +1159,7 @@ let pf_interp_gen_aux ist gl to_ind ((oclr, occ), t) =
   let (c, ucst), cl = 
     try fill_occ_pattern ~raise_NoMatch:true env sigma (EConstr.Unsafe.to_constr cl) pat occ 1
     with NoMatch -> redex_of_pattern env pat, (EConstr.Unsafe.to_constr cl) in
+  let gl = pf_merge_uc ucst gl in
   let c = EConstr.of_constr c in
   let cl = EConstr.of_constr cl in
   let clr = interp_clr sigma (oclr, (tag_of_cpattern t, c)) in
-- 
cgit v1.2.3