diff options
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index ad506b89b2..265994bd65 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -921,7 +921,7 @@ let known_dependent (_,dep) = (dep = KnownDep) let expand_arg tms (p,ccl) ((_,t),_,na) = let k = length_of_tomatch_type_sign na t in - (p+k,liftn_predicate (k-1) p ccl tms) + (p+k,liftn_predicate (k-1) (p+1) ccl tms) let adjust_impossible_cases pb pred tomatch submat = if submat = [] then |