Optimized dependencies for pattern-matching on only trivial patterns.

If a term is matched only against variables, it will not introduce a
"match" and thus, even if the term is of an inductive type, its
indices will not be taken into account in the current algorithm
(though one could imagine an algorithm which does an expansion
specially in order to filter on indices).

This allows to tell the unification not to use dependencies which the
pattern-matching algorithm is not able to exploit in practice.

See example in file 2733.v.

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