aboutsummaryrefslogtreecommitdiff
path: root/plugins/ssr/ssrparser.ml4
diff options
context:
space:
mode:
authorMaxime Dénès2017-11-21 22:24:59 +0100
committerMaxime Dénès2017-11-21 22:24:59 +0100
commiteb91ccaf236bc9a60a1e216b76a0a42980c072a7 (patch)
tree0bc32293ac19ddd63cf764ccbd224b086c7836bc /plugins/ssr/ssrparser.ml4
parentb75beb248873db7d9ab8e4a078022b2ed0edcd36 (diff)
parent0ddf7d9c35eb2dd5f368e7a5735970ef1fd41fc6 (diff)
Merge PR #6173: [printing] Deprecate all printing functions accessing the global proof.
Diffstat (limited to 'plugins/ssr/ssrparser.ml4')
-rw-r--r--plugins/ssr/ssrparser.ml42
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 7b591feada..46403aef3c 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -1131,7 +1131,7 @@ let pr_fwd_guarded prval prval' = function
| (fk, h), (_, (_, Some c)) ->
pr_gen_fwd prval pr_constr_expr prl_constr_expr fk (format_constr_expr h c)
| (fk, h), (_, (c, None)) ->
- pr_gen_fwd prval' pr_glob_constr prl_glob_constr fk (format_glob_constr h c)
+ pr_gen_fwd prval' pr_glob_constr_env prl_glob_constr fk (format_glob_constr h c)
let pr_unguarded prc prlc = prlc