diff options
Diffstat (limited to 'plugins/extraction/mlutil.ml')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 13 |
1 files changed, 6 insertions, 7 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index a8d766cd6e..2d5872718f 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -12,7 +12,6 @@ open Util open Names open Libnames -open Globnames open Table open Miniml (*i*) @@ -668,11 +667,11 @@ let is_regular_match br = | _ -> raise Impossible in let ind = match get_r br.(0) with - | ConstructRef (ind,_) -> ind + | GlobRef.ConstructRef (ind,_) -> ind | _ -> raise Impossible in let is_ref i tr = match get_r tr with - | ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1) + | GlobRef.ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1) | _ -> false in Array.for_all_i is_ref 0 br @@ -819,11 +818,11 @@ let rec tmp_head_lams = function *) let rec ast_glob_subst s t = match t with - | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> + | MLapp ((MLglob ((GlobRef.ConstRef kn) as refe)) as f, a) -> let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in (try linear_beta_red a (Refmap'.find refe s) with Not_found -> MLapp (f, a)) - | MLglob ((ConstRef kn) as refe) -> + | MLglob ((GlobRef.ConstRef kn) as refe) -> (try Refmap'.find refe s with Not_found -> t) | _ -> ast_map (ast_glob_subst s) t @@ -1504,7 +1503,7 @@ open Declareops let inline_test r t = if not (auto_inline ()) then false else - let c = match r with ConstRef c -> c | _ -> assert false in + let c = match r with GlobRef.ConstRef c -> c | _ -> assert false in let has_body = try constant_has_body (Global.lookup_constant c) with Not_found -> false @@ -1534,7 +1533,7 @@ let manual_inline_set = Cset_env.empty let manual_inline = function - | ConstRef c -> Cset_env.mem c manual_inline_set + | GlobRef.ConstRef c -> Cset_env.mem c manual_inline_set | _ -> false (* If the user doesn't say he wants to keep [t], we inline in two cases: |