diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-15 14:07:15 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-02-15 14:07:15 +0100 |
| commit | eec3b87e8cc782cb83ea2eae241129b79c80d496 (patch) | |
| tree | ac1f64c90b03c037556d65fa775714796bcd1b02 | |
| parent | 6a844a236ccef9efb2fb6f86ecba8a6a182a4034 (diff) | |
Fixing bug #3490.
| -rw-r--r-- | pretyping/tacred.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 9d6eb31b4..91cd08844 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -189,6 +189,7 @@ let check_fix_reversibility labs args ((lv,i),(_,tys,bds)) = if Array.for_all (noccurn k) tys && Array.for_all (noccurn (k+nbfix)) bds + && k <= n then (k, List.nth labs (k-1)) else |