diff options
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 2f766afaa6..9c4b64b60d 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1098,7 +1098,8 @@ let is_template_polymorphic_ind env sigma f = let base_sort_cmp pb s0 s1 = match (s0,s1) with - | Prop, Prop | Set, Set | Type _, Type _ -> true + | SProp, SProp | Prop, Prop | Set, Set | Type _, Type _ -> true + | SProp, _ | _, SProp -> false | Prop, Set | Prop, Type _ | Set, Type _ -> pb == Reduction.CUMUL | Set, Prop | Type _, Prop | Type _, Set -> false |