From ce3c7ee7cadcab9a194fb37e0d500948078acda0 Mon Sep 17 00:00:00 2001 From: Julien Forest Date: Mon, 9 Apr 2018 12:02:13 +0200 Subject: removing uggly error message of #5147 --- plugins/funind/functional_principles_types.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'plugins/funind') diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 7a9bbd92c..b3f08301b 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -628,16 +628,19 @@ let build_scheme fas = user_err ~hdr:"FunInd.build_scheme" (str "Cannot find " ++ Libnames.pr_reference f) in - let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in + let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in let _ = evd := evd' in let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in - (destConst f,sort) + if isConst f + then (destConst f,sort) + else user_err Pp.(pr_constr_env (Global.env ()) !evd f ++spc () ++ str "should be a function") ) fas ) in let bodies_types = make_scheme evd pconstants in + List.iter2 (fun (princ_id,_,_) def_entry -> ignore -- cgit v1.2.3