diff options
| author | Pierre-Marie Pédrot | 2019-08-29 14:39:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-08-29 14:39:59 +0200 |
| commit | 60b9352656b95b7e5c46c9f28fec3a171f3fc74a (patch) | |
| tree | fec69b141cf2e71dd9789567b001ca3df55c776b /kernel/uGraph.ml | |
| parent | 737955a82676cab8de7283bf23db3962dd6a3792 (diff) | |
| parent | 94c8f42eea1c36f582fe2390680de75634324c85 (diff) | |
Merge PR #10660: [cleanup] Replace uses of UserError constructor, clarify exception names
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/uGraph.ml')
0 files changed, 0 insertions, 0 deletions