aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/pptactic.ml
diff options
context:
space:
mode:
Diffstat (limited to 'parsing/pptactic.ml')
-rw-r--r--parsing/pptactic.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 58ce29a04..5d03b6028 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -23,6 +23,7 @@ open Printer
open Misctypes
open Locus
open Decl_kinds
+open Genredexpr
let pr_global x = Nametab.pr_global_env Idset.empty x
@@ -650,7 +651,7 @@ and pr_atom1 = function
| TacIntroMove (None,MoveLast) as t -> pr_atom0 t
| TacIntroMove (Some id,MoveLast) -> str "intro " ++ pr_id id
| TacIntroMove (ido,hto) ->
- hov 1 (str"intro" ++ pr_opt pr_id ido ++ Tacops.pr_move_location pr_ident hto)
+ hov 1 (str"intro" ++ pr_opt pr_id ido ++ Miscops.pr_move_location pr_ident hto)
| TacAssumption as t -> pr_atom0 t
| TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
| TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
@@ -764,7 +765,7 @@ and pr_atom1 = function
assert b;
hov 1
(str "move" ++ brk (1,1) ++ pr_ident id1 ++
- Tacops.pr_move_location pr_ident id2)
+ Miscops.pr_move_location pr_ident id2)
| TacRename l ->
hov 1
(str "rename" ++ brk (1,1) ++