diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-08 17:39:02 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-08 17:39:02 +0000 |
| commit | 407ae51db97babb0ffad94abeb89a612c567ec72 (patch) | |
| tree | 7c9f842234137462ddcc6fc94b323d3f9575d740 /plugins/extraction/mlutil.ml | |
| parent | 5e31d0be41febb6d5a54aa4a0d189b41c9bf1c2e (diff) | |
Extraction with implicits: perform the occur-check after optimisations
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13093 85f007b7-540e-0410-9357-904b9bb8a0f7
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 1cef86ee5..034baad95 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 |