diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-04-11 10:16:11 +0200 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-04-11 10:16:11 +0200 |
| commit | 3e69cc44b2a7430881b4425cb5d543c888d9b4c7 (patch) | |
| tree | a1038c42d2e79cd4a9065310fc661e29edeb6791 /plugins/funind | |
| parent | 09ba1e86504c5df554c3bdd1eae05bddcafc6ef2 (diff) | |
| parent | 577738531f607da8e6347ade1dc3767d98aaf863 (diff) | |
Merge PR #7203: removing ugly error message of #5147
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/functional_principles_types.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index 7a9bbd92c..804548ce5 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 the named of a globally defined function") ) fas ) in let bodies_types = make_scheme evd pconstants in + List.iter2 (fun (princ_id,_,_) def_entry -> ignore |