From 213f84e60eda94c90436f0102fed00fe579d0a48 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 12 Dec 2020 16:48:07 +0100
Subject: Tweak constr_matching so as to make it tail-rec on projection
 expansion.

This was revealed on the rewriter contrib with the compact-case-repr branch.
---
 pretyping/constr_matching.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index a3f1c0b004..0e69b814c7 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -528,10 +528,9 @@ let sub_match ?(closed=true) env sigma pat c =
     let sub = subargs env types @ subargs env' bodies in
     try_aux sub next_mk_ctx next
   | Proj (p,c') ->
-    begin try
-      let term = Retyping.expand_projection env sigma p c' [] in
-      aux env term mk_ctx next
-    with Retyping.RetypeError _ -> next ()
+    begin match Retyping.expand_projection env sigma p c' [] with
+    | term -> aux env term mk_ctx next
+    | exception Retyping.RetypeError _ -> next ()
     end
   | Array(u, t, def, ty) ->
     let next_mk_ctx = function
-- 
cgit v1.2.3