From 448866f0ec5291d58677d8fccbefde493ade0ee2 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 Jan 2016 22:20:16 +0100
Subject: Removing constr generic argument.

---
 dev/top_printers.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index cbebcdfcd4..cc1cf23d60 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -510,7 +510,7 @@ let _ =
   try
     Vernacinterp.vinterp_add false ("PrintConstr", 0)
       (function
-         [c] when genarg_tag c = ConstrArgType && true ->
+         [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
            (fun () -> in_current_context constr_display c)
        | _ -> failwith "Vernac extension: cannot occur")
@@ -526,7 +526,7 @@ let _ =
   try
     Vernacinterp.vinterp_add false ("PrintPureConstr", 0)
       (function
-         [c] when genarg_tag c = ConstrArgType && true ->
+         [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
            (fun () -> in_current_context print_pure_constr c)
        | _ -> failwith "Vernac extension: cannot occur")
-- 
cgit v1.2.3