diff options
Diffstat (limited to 'plugins/ltac/g_rewrite.ml4')
| -rw-r--r-- | plugins/ltac/g_rewrite.ml4 | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index fbaa2e58..f1634f15 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -11,7 +11,6 @@ (* Syntax for rewriting with strategies *) open Names -open Misctypes open Locus open Constrexpr open Glob_term @@ -20,9 +19,10 @@ open Extraargs open Tacmach open Rewrite open Stdarg -open Pcoq.Vernac_ +open Tactypes open Pcoq.Prim open Pcoq.Constr +open Pvernac.Vernac_ open Pltac DECLARE PLUGIN "ltac_plugin" @@ -67,13 +67,13 @@ let subst_strategy s str = str let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>" let pr_raw_strategy prc prlc _ (s : raw_strategy) = - let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_reference, prc) in + let prr = Pptactic.pr_red_expr (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc) in Rewrite.pr_strategy prc prr s let pr_glob_strategy prc prlc _ (s : glob_strategy) = let prr = Pptactic.pr_red_expr (Ppconstr.pr_constr_expr, Ppconstr.pr_lconstr_expr, - Pputils.pr_or_by_notation Libnames.pr_reference, + Pputils.pr_or_by_notation Libnames.pr_qualid, Ppconstr.pr_constr_expr) in Rewrite.pr_strategy prc prr s |