1 files changed, 2 insertions, 2 deletions
diff --git a/user-contrib/Ltac2/g_ltac2.mlg b/user-contrib/Ltac2/g_ltac2.mlg
index cc3a7c0f79..c1bd585f3f 100644
--- a/user-contrib/Ltac2/g_ltac2.mlg
+++ b/user-contrib/Ltac2/g_ltac2.mlg
@@ -643,7 +643,7 @@ GRAMMAR EXTEND Gram
   q_conversion:
     [ [ c = conversion -> { c } ] ]
   ;
-  orient:
+  ltac2_orient:
     [ [ "->" -> { CAst.make ~loc (Some true) }
       | "<-" -> { CAst.make ~loc (Some false) }
       | -> { CAst.make ~loc None }
@@ -665,7 +665,7 @@ GRAMMAR EXTEND Gram
       ] ]
   ;
   oriented_rewriter:
-    [ [ b = orient; r = rewriter ->
+    [ [ b = ltac2_orient; r = rewriter ->
       { let (m, c) = r in
         CAst.make ~loc @@ {
         rew_orient = b;