diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 1a527cbeaa..66e3181a3c 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -36,7 +36,7 @@ let abstract_scheme env c l lname_typ = (fun t (locc,a) (na,_,ta) -> if occur_meta ta then error "cannot find a type for the generalisation" else if occur_meta a then lambda_name env (na,ta,t) - else lambda_name env (na,ta,subst_term_occ env locc a t)) + else lambda_name env (na,ta,subst_term_occ locc a t)) c (List.rev l) lname_typ |