diff options
| author |  Cyprien Mangin <cyprien.mangin@m4x.org> | 2018-01-19 10:15:58 +0100 |
|---|---|---|
| committer | Cyprien Mangin <cyprien.mangin@m4x.org> | 2018-01-19 10:15:58 +0100 |
| commit | 2adf81fba2f1b2bb1d7a78a00d2723c103bbf899 (patch) | |
| tree | 1a32fe11b279fd0ec08c7ac13c3a12017bbdbbb2 /pretyping/constr_matching.ml | |
| parent | 248d290aa9313501a857a4d3bd9f3d0dc7dc5b4f (diff) | |
Fix context handling of fix and cofix in Ltac subterm matching.
Diffstat (limited to 'pretyping/constr_matching.ml')
| -rw-r--r-- | pretyping/constr_matching.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index ec7c3077f..c3a221944 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -462,19 +462,21 @@ let sub_match ?(closed=true) env sigma pat c = in let sub = (env, c1) :: (env, hd) :: subargs env lc in try_aux sub next_mk_ctx next - | Fix (indx,(names,types,bodies)) -> + | Fix (indx,(names,types,bodies as recdefs)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkFix (indx,(names, Array.of_list ntypes, Array.of_list nbodies))) in - let sub = subargs env types @ subargs env bodies in + let env' = push_rec_types recdefs env in + let sub = subargs env types @ subargs env' bodies in try_aux sub next_mk_ctx next - | CoFix (i,(names,types,bodies)) -> + | CoFix (i,(names,types,bodies as recdefs)) -> let nb_fix = Array.length types in let next_mk_ctx le = let (ntypes,nbodies) = CList.chop nb_fix le in mk_ctx (mkCoFix (i,(names, Array.of_list ntypes, Array.of_list nbodies))) in - let sub = subargs env types @ subargs env bodies in + let env' = push_rec_types recdefs env in + let sub = subargs env types @ subargs env' bodies in try_aux sub next_mk_ctx next | Proj (p,c') -> begin try |