From 1f7a49374aa2e7a67d1326d02d0d6fb519427ee3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 5 Nov 2017 10:58:03 +0100
Subject: Preventively protect locally against failures of evar_map printer.

It is not clear that this is really needed, but in case it happens,
one will at least have a partial result available rather than an
unexploitable global failure of the parser.
---
 engine/termops.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'engine')

diff --git a/engine/termops.ml b/engine/termops.ml
index b7fa2dc4a4..0f84d7868a 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -327,11 +327,11 @@ let pr_evar_constraints sigma pbs =
       Namegen.make_all_name_different env sigma
     in
     print_env_short env ++ spc () ++ str "|-" ++ spc () ++
-      print_constr_env env sigma (EConstr.of_constr t1) ++ spc () ++
+      protect (print_constr_env env sigma) (EConstr.of_constr t1) ++ spc () ++
       str (match pbty with
             | Reduction.CONV -> "=="
             | Reduction.CUMUL -> "<=") ++
-      spc () ++ print_constr_env env Evd.empty (EConstr.of_constr t2)
+      spc () ++ protect (print_constr_env env Evd.empty) (EConstr.of_constr t2)
   in
   prlist_with_sep fnl pr_evconstr pbs
 
-- 
cgit v1.2.3