diff options
| author | herbelin | 2001-07-24 14:45:36 +0000 |
|---|---|---|
| committer | herbelin | 2001-07-24 14:45:36 +0000 |
| commit | 9ecb3d8a50b7b7f3a79a945a00f445b9a7d89c33 (patch) | |
| tree | 28f493bc447daca8c5076b8c2e10338d29bd2034 | |
| parent | 28d38568e437a09fe3835e2644c4e420dbc4ba51 (diff) | |
Bug Simpl
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1864 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | pretyping/tacred.ml | 3 |
1 files changed, 3 insertions, 0 deletions
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 |