From a1d00fa77939f99dd5e7ddd41c8ecf64e8af4fa1 Mon Sep 17 00:00:00 2001
From: SimonBoulier
Date: Mon, 2 Dec 2019 12:52:39 +0100
Subject: Add syntax for non maximally inserted implicit arguments

---
 plugins/ssr/ssrvernac.mlg | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

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
-- 
cgit v1.2.3