From 2c7d80e8234797da38d54326b914ded7f343d062 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 29 Mar 2015 15:03:19 +0200
Subject: Fixing bug #4165.

The context matching function was dropping the surrounding context in
let-ins.
---
 pretyping/constr_matching.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index cf6ac619dd..f05812979d 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -373,7 +373,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | LetIn (x,c1,t,c2) ->
       let next_mk_ctx = function
-      | [c1;c2] -> mkLetIn (x,c1,t,c2)
+      | [c1; c2] -> mk_ctx (mkLetIn (x, c1, t, c2))
       | _ -> assert false
       in
       let next () = 
-- 
cgit v1.2.3