diff options
| author | Pierre-Marie Pédrot | 2014-09-07 13:20:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-07 13:20:35 +0200 |
| commit | 609ca52bbdde6201056b6226c43e7ffb94d80aa8 (patch) | |
| tree | 451a42f7815c58234c2ac82c9356790aa054c0ac /toplevel/command.ml | |
| parent | cf2dedb50c654f34c06de24507a06c1c9b163363 (diff) | |
Fixing bug #3492.
Diffstat (limited to 'toplevel/command.ml')
| -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 = |