Merge PR #11235: Add syntax for non maximal implicit arguments

Reviewed-by: herbelin
Reviewed-by: jfehrle
Ack-by: maximedenes

1 files changed, 1 insertions, 1 deletions

diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index d8dbf2f3dc..b212e7046a 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -151,7 +151,7 @@ let declare_one_prenex_implicit locality f =
     with _ -> errorstrm (pr_qualid f ++ str " is not declared") in
   let rec loop = function
   | a :: args' when Impargs.is_status_implicit a ->
-    Impargs.MaximallyImplicit :: loop args'
+    MaxImplicit :: loop args'
   | args' when List.exists Impargs.is_status_implicit args' ->
       errorstrm (str "Expected prenex implicits for " ++ pr_qualid f)
   | _ -> [] in