diff options
| author | Hugo Herbelin | 2019-11-18 16:04:45 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-06 17:31:39 +0100 |
| commit | 490704f4b2db98f4ef15f5e380b63e49e13a418b (patch) | |
| tree | 625e60c878e2768dbce36129e1df80ceace17495 /plugins/firstorder | |
| parent | 28c4f57e0614523879201d1c59816cde188e5b22 (diff) | |
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.
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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 " : " ++ |