diff options
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 () ++ |