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

6 files changed, 46 insertions, 14 deletions

diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index a65b3941e..9ac16b5b4 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -695,6 +695,10 @@ let cast_rel_context :
   type a b. (a,b) eq -> (a, a) Rel.pt -> (b, b) Rel.pt =
   fun Refl x -> x
 
+let cast_rec_decl :
+  type a b. (a,b) eq -> (a, a) Constr.prec_declaration -> (b, b) Constr.prec_declaration =
+  fun Refl x -> x
+
 let cast_named_decl :
   type a b. (a,b) eq -> (a, a) Named.Declaration.pt -> (b, b) Named.Declaration.pt =
   fun Refl x -> x
@@ -817,6 +821,7 @@ let it_mkLambda_or_LetIn t ctx = List.fold_left (fun c d -> mkLambda_or_LetIn d
 
 let push_rel d e = push_rel (cast_rel_decl unsafe_eq d) e
 let push_rel_context d e = push_rel_context (cast_rel_context unsafe_eq d) e
+let push_rec_types d e = push_rec_types (cast_rec_decl unsafe_eq d) e
 let push_named d e = push_named (cast_named_decl unsafe_eq d) e
 let push_named_context d e = push_named_context (cast_named_context unsafe_eq d) e
 let push_named_context_val d e = push_named_context_val (cast_named_decl unsafe_eq d) e
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 30de748a1..6fa338c73 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -251,6 +251,7 @@ end
 
 val push_rel : rel_declaration -> env -> env
 val push_rel_context : rel_context -> env -> env
+val push_rec_types : (t, t) Constr.prec_declaration -> env -> env
 
 val push_named : named_declaration -> env -> env
 val push_named_context : named_context -> env -> env
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
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 788e4d268..41c4616f7 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 43066c809..3132d2ad5 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
diff --git a/test-suite/bugs/closed/6617.v b/test-suite/bugs/closed/6617.v
new file mode 100644
index 000000000..9cabd62d4
--- /dev/null
+++ b/test-suite/bugs/closed/6617.v
@@ -0,0 +1,34 @@
+Definition MR {T M : Type} :=
+fun (R : M -> M -> Prop) (m : T -> M) (x y : T) => R (m x) (m y).
+
+Set Primitive Projections.
+
+Record sigma {A : Type} {B : A -> Type} : Type := sigmaI
+  { pr1 : A;  pr2 : B pr1 }.
+
+Axiom F : forall {A : Type} {R : A -> A -> Prop},
+  (forall x, (forall y, R y x -> unit) -> unit) -> forall (x : A), unit.
+
+Definition foo (A : Type) (l : list A) :=
+  let y := {| pr1 := A; pr2 := l |} in
+  let bar := MR lt (fun p : sigma =>
+                 (fix Ffix (x : list (pr1 p)) : nat :=
+                    match x with
+                    | nil => 0
+                    | cons _ x1 => S (Ffix x1)
+                    end) (pr2 p)) in
+fun (_ : bar y y) =>
+F (fun (r : sigma)
+       (X : forall q : sigma, bar q r -> unit) => tt).
+
+Definition fooT (A : Type) (l : list A) : Type :=
+  ltac:(let ty := type of (foo A l) in exact ty).
+Parameter P : forall A l, fooT A l -> Prop.
+
+Goal forall A l, P A l (foo A l).
+Proof.
+  intros; unfold foo.
+  Fail match goal with
+    | [ |- context [False]] => idtac
+  end.
+Admitted.