diff options
| author | herbelin | 2011-10-22 12:34:08 +0000 |
|---|---|---|
| committer | herbelin | 2011-10-22 12:34:08 +0000 |
| commit | 56d4015ec3e49d2cfba90d6617e041a365bdeec9 (patch) | |
| tree | ca2914c811ca38b4f1f02395e0fc21e416d359e0 /tactics | |
| parent | 1ffb37b4651dcc7a2b1d59285e07ea9e2a3febe5 (diff) | |
Fixing Equality.injectable which did not detect an equality without
constructors as non relevant for injection. Also made injection
failing in such situation.
Incidentally, this fixes a loop in Invfun.reflexivity_with_destruct_cases
(observed in the compilation of CoinductiveReals.LNP_Digit). The
most probable explanation is that this loop was formerly protected by
a failing rewrite which stopped failing after revision 14549 made
second-order pattern-matching more powerful.
Also suppressed dead code in Invfun.intros_with_rewrite.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14577 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 2d4268e60e..b037ea7e2a 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -568,7 +568,7 @@ let discriminable env sigma t1 t2 = let injectable env sigma t1 t2 = match find_positions env sigma t1 t2 with - | Inl _ | Inr [] -> false + | Inl _ | Inr [] | Inr [([],_,_)] -> false | Inr _ -> true @@ -1112,6 +1112,8 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause = | Inr [] -> errorlabstrm "Equality.inj" (str"Nothing to do, it is an equality between convertible terms.") + | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 -> + errorlabstrm "Equality.inj" (str"Nothing to inject.") | Inr posns -> (* Est-ce utile à partir du moment où les arguments projetés subissent "nf" ? let t1 = try_delta_expand env sigma t1 in |