From 609ca52bbdde6201056b6226c43e7ffb94d80aa8 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 7 Sep 2014 13:20:35 +0200
Subject: Fixing bug #3492.

---
 toplevel/command.ml | 3 +++
 1 file changed, 3 insertions(+)

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 =
-- 
cgit v1.2.3