diff options
| author | Hugo Herbelin | 2015-10-19 16:06:46 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2015-10-19 16:08:17 +0200 |
| commit | c3967bd7a71df53a004478d23b072309f13f2ff5 (patch) | |
| tree | 4af71612aa02f318d1d7b1a7d0ba2738bdb7966b | |
| parent | 70d3ad33f6ba7a1c6b1fb93aadd5c05d7e9c03b8 (diff) | |
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.
| -rw-r--r-- | tactics/equality.ml | 9 |
1 files changed, 8 insertions, 1 deletions
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 |