diff options
| author | Pierre-Marie Pédrot | 2015-03-29 15:03:19 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-03-29 15:03:19 +0200 |
| commit | 2c7d80e8234797da38d54326b914ded7f343d062 (patch) | |
| tree | 360b81c39dcf39019f185b3038a47a0cb0f74ff0 | |
| parent | f3ff16adced3e5bf8d11cb74ee68be1267edc2b6 (diff) | |
Fixing bug #4165.
The context matching function was dropping the surrounding context in
let-ins.
| -rw-r--r-- | pretyping/constr_matching.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 () = |