diff options
| author | Matthieu Sozeau | 2015-10-14 16:39:09 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2015-10-14 17:06:49 +0200 |
| commit | b8c681338cad546c397a1803c55183cc6526adfb (patch) | |
| tree | 9eb2e8e420676e4e0a54a7cddd5475ef5cb21eca | |
| parent | 5009be2f117a5ef27733b7d6895503af91e9aa34 (diff) | |
Fix constr_matching when a match is found in the head of a case construct
| -rw-r--r-- | pretyping/constr_matching.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 19c85c9e27..121ab74885 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -415,8 +415,8 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c = try_aux sub mk_ctx next | Case (ci,hd,c1,lc) -> let next_mk_ctx = function - | [] -> assert false - | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) + | c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc)) + | _ -> assert false in let sub = (env, c1) :: (env, hd) :: subargs env lc in try_aux sub next_mk_ctx next |