Merge PR #6618: Fix Ltac subterm matching in (co-)fixpoints.

3 files changed, 6 insertions, 14 deletions

diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index ec7c3077fb..c3a221944d 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
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 788e4d268a..41c4616f79 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -276,11 +276,6 @@ let rec ise_app_stack2 env f evd sk1 sk2 =
      end
   | _, _ -> (sk1,sk2), Success evd
 
-let push_rec_types pfix env =
-  let (i, c, t) = pfix in
-  let inj c = EConstr.Unsafe.to_constr c in
-  push_rec_types (i, Array.map inj c, Array.map inj t) env
-
 (* This function tries to unify 2 stacks element by element. It works
    from the end to the beginning. If it unifies a non empty suffix of
    stacks but not the entire stacks, the first part of the answer is
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 43066c8099..3132d2ad53 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -23,11 +23,6 @@ open Arguments_renaming
 open Pretype_errors
 open Context.Rel.Declaration
 
-let push_rec_types pfix env =
-  let (i, c, t) = pfix in
-  let inj c = EConstr.Unsafe.to_constr c in
-  push_rec_types (i, Array.map inj c, Array.map inj t) env
-
 let meta_type evd mv =
   let ty =
     try Evd.meta_ftype evd mv