diff options
| author | Pierre-Marie Pédrot | 2019-10-30 14:18:37 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-30 14:18:37 +0100 |
| commit | 964e3f409b4db3c682913a4d90394e96453a1274 (patch) | |
| tree | 072e0b588ad881816dde47d9cd8796bbcc0d081b /dev/include_dune | |
| parent | 7634426a7a6de08ff0ea172a0770b9a159b25934 (diff) | |
| parent | d13e7e924437b043f83b6a47bfefda69379264b7 (diff) | |
Merge PR #10303: Raise an anomaly when looking up unknown constant/inductive
Reviewed-by: ppedrot
Diffstat (limited to 'dev/include_dune')
0 files changed, 0 insertions, 0 deletions