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 19e0a9ade7..2d0e96a2fc 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -28,7 +28,7 @@ let prop_name = id_of_string "_" let rec update_args sp vl = function | Tapp ( Tglob r :: l ) -> (match r with - | IndRef (s,_) when s = sp -> Tapp ( Tglob r :: vl) + | IndRef (s,_) when s = sp -> Tapp ( Tglob r :: l @ vl ) | _ -> Tapp (Tglob r :: (List.map (update_args sp vl) l))) | Tapp l -> Tapp (List.map (update_args sp vl) l) | Tarr (a,b)-> |