From 7f15ecab95ec79f15211115799f1480fc1389c06 Mon Sep 17 00:00:00 2001
From: barras
Date: Tue, 9 Mar 2004 15:32:18 +0000
Subject: bug de l'inversion (coq-bugs #529)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5444 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 cabbdba869..bda850f84f 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -683,7 +683,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
 	| Some w -> applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
 	| None -> anomaly "Not enough components to build the dependent tuple"
   in
-  sigrec_clausal_form siglen ty
+  Evarutil.nf_evar (Evarutil.evars_of isevars) (sigrec_clausal_form siglen ty)
 
 (* The problem is to build a destructor (a generalization of the
    predecessor) which, when applied to a term made of constructors
-- 
cgit v1.2.3