diff options
| author | Pierre-Marie Pédrot | 2020-10-29 13:59:45 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-12-21 13:55:32 +0100 |
| commit | 63332cbd4ac59b39fdce63d9872aa52dd8a2fec6 (patch) | |
| tree | 9913737179ee72e0c1b9672227fe5872ce6734a9 /user-contrib | |
| parent | a714abe0a1c0cac277297f9e3c7f6d90ac0173d6 (diff) | |
Move evaluable_global_reference from Names to Tacred.
It is the only place where it starts making sense in the whole codebase. It also
fits nicely there since there are other functions manipulating this type in that
module.
In any case this type does not belong to the kernel.
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/tac2tactics.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml index 69758b3f37..54f5a2cf68 100644 --- a/user-contrib/Ltac2/tac2tactics.ml +++ b/user-contrib/Ltac2/tac2tactics.ml @@ -209,13 +209,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 (GlobRef.ConstRef cst) -> (mk_occurrences_expr occ, Inl (EvalConstRef cst)) -| Pattern.PRef (GlobRef.VarRef id) -> (mk_occurrences_expr occ, Inl (EvalVarRef id)) +| Pattern.PRef (GlobRef.ConstRef cst) -> (mk_occurrences_expr occ, Inl (Tacred.EvalConstRef cst)) +| Pattern.PRef (GlobRef.VarRef id) -> (mk_occurrences_expr occ, Inl (Tacred.EvalVarRef id)) | _ -> (mk_occurrences_expr occ, Inr pat) let get_evaluable_reference = function -| GlobRef.VarRef id -> Proofview.tclUNIT (EvalVarRef id) -| GlobRef.ConstRef cst -> Proofview.tclUNIT (EvalConstRef cst) +| GlobRef.VarRef id -> Proofview.tclUNIT (Tacred.EvalVarRef id) +| GlobRef.ConstRef cst -> Proofview.tclUNIT (Tacred.EvalConstRef cst) | r -> Tacticals.New.tclZEROMSG (str "Cannot coerce" ++ spc () ++ Nametab.pr_global_env Id.Set.empty r ++ spc () ++ |