diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 58dda021..1f7bdad3 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 9215 2006-10-05 15:40:31Z herbelin $ *) +(* $Id: cases.ml 10071 2007-08-10 15:34:41Z herbelin $ *) open Util open Names @@ -1021,18 +1021,18 @@ let abstract_predicate env sigma indf cur tms = function (* Depending on whether the predicate is dependent or not, and has real args or not, we lift it to make room for [sign] *) (* Even if not intrinsically dep, we move the predicate into a dep one *) - let sign,k = + let sign,q = if names = [] & n <> 1 then (* Real args were not considered *) (if dep<>Anonymous then - ((let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign),n-1) + (let (_,c,t) = List.hd sign in (dep,c,t)::List.tl sign) else - (sign,n)) + sign),n else (* Real args are OK *) - (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign, - if dep<>Anonymous then 0 else 1) in - let pred = lift_predicate k pred in + (List.map2 (fun na (_,c,t) -> (na,c,t)) (dep::names) sign,1) in + let q,k = if dep <> Anonymous then (q-1,2) else (q,1) in + let pred = liftn_predicate q k pred in let pred = extract_predicate [] (pred,tms) in (true, it_mkLambda_or_LetIn_name env pred sign) |