diff options
Diffstat (limited to 'plugins/extraction/mlutil.ml')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 1cef86ee59..034baad955 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -497,8 +497,6 @@ let ast_subst e = [v] array: [(Rel i)] becomes [v.(i-1)]. [d] is the correction applies to [Rel] greater than [Array.length v]. *) -exception Occurs of int - let gen_subst v d t = let rec subst n = function | MLrel i as a -> @@ -506,7 +504,7 @@ let gen_subst v d t = if i' < 1 then a else if i' <= Array.length v then match v.(i'-1) with - | None -> raise (Occurs i') + | None -> MLexn ("UNBOUND " ^ string_of_int i') | Some u -> ast_lift n u else MLrel (i+d) | a -> ast_map_lift subst n a |