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/haskell.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/haskell.ml')
| -rw-r--r-- | plugins/extraction/haskell.ml | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index a62fb1a728..e4efbcff0c 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -14,7 +14,6 @@ open Pp open CErrors open Util open Names -open Globnames open Table open Miniml open Mlutil @@ -110,7 +109,7 @@ let rec pp_type par vl t = (try Id.print (List.nth vl (pred i)) with Failure _ -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global Type r - | Tglob (IndRef(kn,0),l) + | Tglob (GlobRef.IndRef(kn,0),l) when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") -> pp_type true vl (List.hd l) | Tglob (r,l) -> @@ -271,7 +270,7 @@ let pp_logical_ind packet = prvect_with_sep spc Id.print packet.ip_consnames) let pp_singleton kn packet = - let name = pp_global Type (IndRef (kn,0)) in + let name = pp_global Type (GlobRef.IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in hov 2 (str "type " ++ name ++ spc () ++ prlist_with_sep spc Id.print l ++ @@ -291,14 +290,14 @@ let pp_one_ind ip pl cv = (fun () -> (str " ")) (pp_type true pl) l)) in str (if Array.is_empty cv then "type " else "data ") ++ - pp_global Type (IndRef ip) ++ + pp_global Type (GlobRef.IndRef ip) ++ prlist_strict (fun id -> str " " ++ pr_lower_id id) pl ++ str " =" ++ if Array.is_empty cv then str " () -- empty inductive" else (fnl () ++ str " " ++ v 0 (str " " ++ prvect_with_sep (fun () -> fnl () ++ str "| ") pp_constructor - (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv))) + (Array.mapi (fun i c -> GlobRef.ConstructRef (ip,i+1),c) cv))) let rec pp_ind first kn i ind = if i >= Array.length ind.ind_packets then @@ -306,7 +305,7 @@ let rec pp_ind first kn i ind = else let ip = (kn,i) in let p = ind.ind_packets.(i) in - if is_custom (IndRef (kn,i)) then pp_ind first kn (i+1) ind + if is_custom (GlobRef.IndRef (kn,i)) then pp_ind first kn (i+1) ind else if p.ip_logical then pp_logical_ind p ++ pp_ind first kn (i+1) ind |