aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/ssr/ssrvernac.mlg2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 24772a8514..4a907b2795 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -159,7 +159,7 @@ let declare_one_prenex_implicit locality f =
| [] ->
errorstrm (str "Expected some implicits for " ++ pr_qualid f)
| impls ->
- Impargs.set_implicits locality fref [impls]
+ Impargs.set_implicits locality fref [List.map (fun imp -> (Anonymous,imp)) impls]
}