diff options
| -rw-r--r-- | toplevel/command.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 18f5afa4b0..582dde30d3 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -362,6 +362,9 @@ let interp_ind_arity evdref env ind = let imps = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in let t, impls = understand_tcc_evars evdref env ~expected_type:IsType c, imps in let pseudo_poly = check_anonymous_type c in + let () = if not (Reduction.is_arity env t) then + user_err_loc (constr_loc ind.ind_arity, "", str "Not an arity") + in t, pseudo_poly, impls let interp_cstrs evdref env impls mldata arity ind = |