aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/command.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/command.ml')
-rw-r--r--toplevel/command.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 5041d78a3..1fda5b9f7 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -548,6 +548,7 @@ let check_param = function
| LocalRawDef (na, _) -> check_named na
| LocalRawAssum (nas, Default _, _) -> List.iter check_named nas
| LocalRawAssum (nas, Generalized _, _) -> ()
+| LocalPattern _ -> assert false
let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
check_all_names_different indl;