diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-17 08:47:12 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-10-17 08:47:12 +0000 |
| commit | 540a93a8e6665f70b2a61158728d6b85be101274 (patch) | |
| tree | 9f662d09d29efe2a2dd3327600b5c1247922a299 | |
| parent | 32c747754e958e5a93ae45af83fb28887a88eaf9 (diff) | |
Vérification de la typability de 'pattern'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6226 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 *) |