diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-05 10:58:03 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-05 10:58:03 +0100 |
| commit | 1f7a49374aa2e7a67d1326d02d0d6fb519427ee3 (patch) | |
| tree | bd0a73163e69ad7425545b496bcb234bdf300686 /engine/termops.ml | |
| parent | 0b2e6fe634da336ed34dec93072e847a1736afd2 (diff) | |
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.
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index b7fa2dc4a..0f84d7868 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 |