From 490704f4b2db98f4ef15f5e380b63e49e13a418b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 18 Nov 2019 16:04:45 +0100
Subject: Moving the diversity of constr printers to a label style.

This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
---
 plugins/firstorder/sequent.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 9ff05c33e4..7d84ee6851 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -231,7 +231,7 @@ let print_cmap map=
   let print_entry c l s=
     let env = Global.env () in
     let sigma = Evd.from_env env in
-    let xc=Constrextern.extern_constr false env sigma (EConstr.of_constr c) in
+    let xc=Constrextern.extern_constr env sigma (EConstr.of_constr c) in
       str "| " ++
       prlist Printer.pr_global l ++
       str " : " ++
-- 
cgit v1.2.3