diff options
| author | Emilio Jesus Gallego Arias | 2019-06-21 22:50:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-08 15:59:10 +0200 |
| commit | c51fb2fae0e196012de47203b8a71c61720d6c5c (patch) | |
| tree | e49c2d38b6c841dc6514944750d21ed08ab94bce /plugins/extraction/mlutil.ml | |
| parent | 437063a0c745094c5693d1c5abba46ce375d69c6 (diff) | |
[api] Deprecate GlobRef constructors.
Not pretty, but it had to be done some day, as `Globnames` seems to be
on the way out.
I have taken the opportunity to reduce the number of `open` in the
codebase.
The qualified style would indeed allow us to use a bit nicer names
`GlobRef.Inductive` instead of `IndRef`, etc... once we have the
tooling to do large-scale refactoring that could be tried.
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: |