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 /user-contrib/Ltac2/tac2tactics.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 'user-contrib/Ltac2/tac2tactics.ml')
| -rw-r--r-- | user-contrib/Ltac2/tac2tactics.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml index 6c96ef7742..561bd9c0c5 100644 --- a/user-contrib/Ltac2/tac2tactics.ml +++ b/user-contrib/Ltac2/tac2tactics.ml @@ -11,7 +11,6 @@ open Pp open Util open Names -open Globnames open Tac2types open Tac2extffi open Genredexpr @@ -209,13 +208,13 @@ let letin_pat_tac ev ipat na c cl = Instead, we parse indifferently any pattern and dispatch when the tactic is called. *) let map_pattern_with_occs (pat, occ) = match pat with -| Pattern.PRef (ConstRef cst) -> (mk_occurrences_expr occ, Inl (EvalConstRef cst)) -| Pattern.PRef (VarRef id) -> (mk_occurrences_expr occ, Inl (EvalVarRef id)) +| Pattern.PRef (GlobRef.ConstRef cst) -> (mk_occurrences_expr occ, Inl (EvalConstRef cst)) +| Pattern.PRef (GlobRef.VarRef id) -> (mk_occurrences_expr occ, Inl (EvalVarRef id)) | _ -> (mk_occurrences_expr occ, Inr pat) let get_evaluable_reference = function -| VarRef id -> Proofview.tclUNIT (EvalVarRef id) -| ConstRef cst -> Proofview.tclUNIT (EvalConstRef cst) +| GlobRef.VarRef id -> Proofview.tclUNIT (EvalVarRef id) +| GlobRef.ConstRef cst -> Proofview.tclUNIT (EvalConstRef cst) | r -> Tacticals.New.tclZEROMSG (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++ spc () ++ |