Merge PR #7274: Avoiding introducing dependency on the indices of a term which has no matching clauses.

2 files changed, 21 insertions, 0 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 6a63fb02f8..ad33297f0a 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -373,6 +373,11 @@ let ltac_interp_realnames lvar = function
   | t, IsInd (ty,ind,realnal) -> t, IsInd (ty,ind,List.map (ltac_interp_name lvar) realnal)
   | _ as x -> x
 
+let is_patvar pat =
+  match DAst.get pat with
+  | PatVar _ -> true
+  | _ -> false
+
 let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) =
   let loc = loc_of_glob_constr tomatch in
   let tycon,realnames = find_tomatch_tycon evdref env loc indopt in
@@ -381,6 +386,7 @@ let coerce_row typing_fun evdref env lvar pats (tomatch,(na,indopt)) =
   let typ = nf_evar !evdref j.uj_type in
   lvar := make_return_predicate_ltac_lvar !evdref na tomatch j.uj_val !lvar;
   let t =
+    if realnames = None && pats <> [] && List.for_all is_patvar pats then NotInd (None,typ) else
     try try_find_ind env !evdref typ realnames
     with Not_found ->
       unify_tomatch_with_patterns evdref env loc typ pats realnames in
diff --git a/test-suite/bugs/closed/2733.v b/test-suite/bugs/closed/2733.v
index 832de4f913..24dd30b32e 100644
--- a/test-suite/bugs/closed/2733.v
+++ b/test-suite/bugs/closed/2733.v
@@ -16,6 +16,21 @@ match k,l with
  |B,l' => Bcons true (Ncons 0 l')
 end.
 
+(* At some time, the success of trullynul was dependent on the name of
+   the variables! *)
+
+Definition trullynul2 k {a} (l : alt_list k a) :=
+match k,l with
+ |N,l' => Ncons 0 (Bcons true l')
+ |B,l' => Bcons true (Ncons 0 l')
+end.
+
+Definition trullynul3 k {z} (l : alt_list k z) :=
+match k,l with
+ |N,l' => Ncons 0 (Bcons true l')
+ |B,l' => Bcons true (Ncons 0 l')
+end.
+
 Fixpoint app (P : forall {k k'}, alt_list k k' -> alt_list k k') {t1 t2} (l : alt_list t1 t2) {struct l}: forall {t3}, alt_list t2 t3 ->
 alt_list t1 t3 :=
   match l with