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/ssrmatching | |
| 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/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 7fc1a12b61..17db25660f 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -361,7 +361,7 @@ type tpattern = { let all_ok _ _ = true let proj_nparams c = - try 1 + Recordops.find_projection_nparams (ConstRef c) with _ -> 0 + try 1 + Recordops.find_projection_nparams (GlobRef.ConstRef c) with _ -> 0 let isRigid c = match kind c with | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true @@ -454,7 +454,7 @@ let ungen_upat lhs (sigma, uc, t) u = let nb_cs_proj_args pc f u = let na k = - List.length (snd (lookup_canonical_conversion (ConstRef pc, k))).o_TCOMPS in + List.length (snd (lookup_canonical_conversion (GlobRef.ConstRef pc, k))).o_TCOMPS in let nargs_of_proj t = match kind t with | App(_,args) -> Array.length args | Proj _ -> 0 (* if splay_app calls expand_projection, this has to be @@ -928,7 +928,7 @@ let id_of_cpattern (_, (c1, c2), _) = Some (qualid_basename qid) | _, Some { v = CAppExpl ((_, qid, _), []) } when qualid_is_ident qid -> Some (qualid_basename qid) - | GRef (VarRef x, _), None -> Some x + | GRef (GlobRef.VarRef x, _), None -> Some x | _ -> None let id_of_Cterm t = match id_of_cpattern t with | Some x -> x @@ -1267,7 +1267,7 @@ let pf_fill_occ_term gl occ t = cl, t let cpattern_of_id id = - ' ', (DAst.make @@ GRef (VarRef id, None), None), Some Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty }) + ' ', (DAst.make @@ GRef (GlobRef.VarRef id, None), None), Some Geninterp.({ lfun = Id.Map.empty; poly = false; extra = Tacinterp.TacStore.empty }) let is_wildcard ((_, (l, r), _) : cpattern) : bool = match DAst.get l, r with | _, Some { CAst.v = CHole _ } | GHole _, None -> true |