diff options
| author | Pierre Letouzey | 2014-12-09 12:48:32 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-12-09 14:27:21 +0100 |
| commit | af84e080ff674a3d5cf2cf88874ddb6ebaf38ecf (patch) | |
| tree | b8325cd8ce34dd2dcfba2792a0123cf8c46ab703 /pretyping/termops.ml | |
| parent | 9c24cecec3a7381cd924c56ca50c77a49750e2e5 (diff) | |
Switch the few remaining iso-latin-1 files to utf8
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 75c8fb4246..72f87a19ea 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -851,9 +851,9 @@ let align_prod_letin c a : rel_context * constr = let (l1,l2) = Util.List.chop lc l in l2,it_mkProd_or_LetIn a l1 -(* On reduit une serie d'eta-redex de tete ou rien du tout *) +(* We reduce a series of head eta-redex or nothing at all *) (* [x1:c1;...;xn:cn]@(f;a1...an;x1;...;xn) --> @(f;a1...an) *) -(* Remplace 2 versions précédentes buggées *) +(* Remplace 2 earlier buggish versions *) let rec eta_reduce_head c = match kind_of_term c with |