From c3967bd7a71df53a004478d23b072309f13f2ff5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 19 Oct 2015 16:06:46 +0200
Subject: Turning anomaly into error for #4372 (weakness of inversion in the
 presence of dependent types with only superficial dependency).

See discussion at https://coq.inria.fr/bugs/show_bug.cgi?id=4372.
---
 tactics/equality.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 5ed9ac2ba0..bc711b81ef 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1126,7 +1126,14 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
               applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
             else
               error "Cannot solve a unification problem."
-	| None -> anomaly (Pp.str "Not enough components to build the dependent tuple")
+	| None ->
+            (* This at least happens if what has been detected as a
+               dependency is not one; use an evasive error message;
+               even if the problem is upwards: unification should be
+               tried in the first place in make_iterated_tuple instead
+               of approximatively computing the free rels; then
+               unsolved evars would mean not binding rel *)
+	    error "Cannot solve a unification problem."
   in
   let scf = sigrec_clausal_form siglen ty in
     !evdref, Evarutil.nf_evar !evdref scf
-- 
cgit v1.2.3