From 55a45dcd9c88119e167277be3dc33e48dcc8910b Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 11 Oct 2003 15:48:12 +0000
Subject: Uniformisation comportement decompEq pour corriger un bug introduit
 dans le Inversion acceptant le nommage des hypotheses

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4602 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/equality.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 9bd3254ec3..6fecc64984 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -861,7 +861,7 @@ let decompEqThen ntac id gls =
 	       ([onLastHyp gen_absurdity;
 		 refine (mkApp (pf, [| mkVar id |]))]))) gls
      | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
-         tclIDTAC gls
+         ntac 0 gls
      | Inr posns ->
 	 (let e = pf_get_new_id (id_of_string "e") gls in
 	  let e_env = push_named (e,None,t) env in
-- 
cgit v1.2.3