From 5e436269003ba9e6db4d0e94dfe571b42e5d13fd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 12 Mar 2004 17:16:59 +0000
Subject: Retablissement de la correction bug d'inversion faite dans la version
 1.116 et malencontreusement passe a la trappe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5469 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 564e7638a8..22436504d4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -624,7 +624,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