diff options
Diffstat (limited to 'vernac/command.ml')
| -rw-r--r-- | vernac/command.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/vernac/command.ml b/vernac/command.ml index 1f1464856..446afb578 100644 --- a/vernac/command.ml +++ b/vernac/command.ml @@ -422,13 +422,13 @@ let prepare_param = function let rec check_anonymous_type ind = let open Glob_term in - match ind with - | GSort (_, GType []) -> true - | GProd (_, _, _, _, e) - | GLetIn (_, _, _, _, e) - | GLambda (_, _, _, _, e) - | GApp (_, e, _) - | GCast (_, e, _) -> check_anonymous_type e + match snd ind with + | GSort (GType []) -> true + | GProd ( _, _, _, e) + | GLetIn (_, _, _, e) + | GLambda (_, _, _, e) + | GApp (e, _) + | GCast (e, _) -> check_anonymous_type e | _ -> false let make_conclusion_flexible evdref ty poly = |