diff options
Diffstat (limited to 'contrib/extraction/mlutil.ml')
| -rw-r--r-- | contrib/extraction/mlutil.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 804416a6d9..721a77b7c3 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -261,7 +261,7 @@ let rec anonym_lams a = function let rec dummy_lams a = function | 0 -> a - | n -> anonym_lams (MLlam (dummy_name,a)) (pred n) + | n -> dummy_lams (MLlam (dummy_name,a)) (pred n) (*S Operations concerning eta. *) |