diff options
| author | Hugo Herbelin | 2016-07-31 07:57:13 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-08-17 10:32:55 +0200 |
| commit | 979b7cbba63f6c033bab40ad5c552572ab5d7d71 (patch) | |
| tree | 0e81c375b96b6ab2e1e054a63ae05afdcd3b9f8c /pretyping/pretype_errors.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 'pretyping/pretype_errors.ml')
0 files changed, 0 insertions, 0 deletions