aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/command.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/command.ml')
-rw-r--r--vernac/command.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/command.ml b/vernac/command.ml
index 12df344c2..cae33f316 100644
--- a/vernac/command.ml
+++ b/vernac/command.ml
@@ -422,7 +422,7 @@ let prepare_param = function
let rec check_anonymous_type ind =
let open Glob_term in
- match snd ind with
+ match ind.CAst.v with
| GSort (GType []) -> true
| GProd ( _, _, _, e)
| GLetIn (_, _, _, e)