diff options
Diffstat (limited to 'contrib/extraction/mlutil.ml')
| -rw-r--r-- | contrib/extraction/mlutil.ml | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 52798cb58..d9286f441 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -319,7 +319,6 @@ let rec permut_case_fun br acc = done; (ids,br) - (*s Generalized iota-reduction. *) (* Definition of a generalized iota-redex: it's a [MLcase(e,_)] |