From 9ecb3d8a50b7b7f3a79a945a00f445b9a7d89c33 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 24 Jul 2001 14:45:36 +0000
Subject: Bug Simpl

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1864 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/tacred.ml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index e56533c51c..abbd47b8b1 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -98,8 +98,11 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) =
   if list_distinct (List.map fst li) then 
     let k = lv.(i) in
     if k < nargs then
+(*  Such an optimisation would need eta-expansion 
       let p = destRel (List.nth args k) in 
       EliminationFix (n-p+1,(nbfix,li,n))
+*)
+      EliminationFix (n,(nbfix,li,n))
     else
       EliminationFix (n-nargs+lv.(i)+1,(nbfix,li,n))
   else 
-- 
cgit v1.2.3