diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-07-31 07:57:13 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-08-17 10:32:55 +0200 |
commit | 979b7cbba63f6c033bab40ad5c552572ab5d7d71 (patch) | |
tree | 0e81c375b96b6ab2e1e054a63ae05afdcd3b9f8c /lib/cWarnings.ml | |
parent | 5cd253c4d8e046d7eac108b48be2d510c114a49a (diff) |
Two protections against failures when printing evar_map.
Delimit the scope of the failure to ease potential need for debugging
the debugging printer.
Protect against one of the causes of failure (calling
get_family_sort_of with non-synchronized sigma).
Diffstat (limited to 'lib/cWarnings.ml')
0 files changed, 0 insertions, 0 deletions