diff options
Diffstat (limited to 'tactics/tacticals.ml')
| -rw-r--r-- | tactics/tacticals.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 6e3d331218..168cd94e1c 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -313,9 +313,9 @@ let elimination_sort_of_goal gl = match kind_of_term (hnf_type_of gl (pf_concl gl)) with | IsSort s -> (match s with - | Prop Null -> ElimOnProp - | Prop Pos -> ElimOnSet - | Type _ -> ElimOnType) + | Prop Null -> InProp + | Prop Pos -> InSet + | Type _ -> InType) | _ -> anomaly "goal should be a type" |