diff options
| -rw-r--r-- | pretyping/tacred.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 88928d97f..a48881bd7 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -795,18 +795,18 @@ let compute = cbv_betadeltaiota (* gives [na:ta]c' such that c converts to ([na:ta]c' a), abstracting only * the specified occurrences. *) -let abstract_scheme env sigma (locc,a) t = +let abstract_scheme env sigma (locc,a) c = let ta = Retyping.get_type_of env sigma a in let na = named_hd env ta Anonymous in if occur_meta ta then error "cannot find a type for the generalisation"; if occur_meta a then - mkLambda (na,ta,t) + mkLambda (na,ta,c) else - mkLambda (na, ta,subst_term_occ locc a t) - + mkLambda (na,ta,subst_term_occ locc a c) let pattern_occs loccs_trm env sigma c = let abstr_trm = List.fold_right (abstract_scheme env sigma) loccs_trm c in + let _ = Typing.type_of env sigma abstr_trm in applist(abstr_trm, List.map snd loccs_trm) (* Generic reduction: reduction functions used in reduction tactics *) |