diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/taccoerce.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 026c00b849..fcab98c7e8 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -199,7 +199,8 @@ let id_of_name = function basename | Sort s -> begin - match ESorts.kind sigma s with + match ESorts.kind sigma s with + | Sorts.SProp -> Label.to_id (Label.make "SProp") | Sorts.Prop -> Label.to_id (Label.make "Prop") | Sorts.Set -> Label.to_id (Label.make "Set") | Sorts.Type _ -> Label.to_id (Label.make "Type") |