From 2350a6042b08d3793dc2fac535fadfaa623ac549 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 23 Nov 2013 11:56:30 +0100 Subject: Fixing bug #3165. --- interp/constrintern.ml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 8337e96f0..b957f317a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -895,9 +895,15 @@ let chop_params_pattern loc ind args with_letin = args let find_constructor loc add_params ref = - let cstr = (function ConstructRef cstr -> cstr - |IndRef _ -> user_err_loc (loc,"find_constructor",str "There is an inductive name deep in a \"in\" clause.") - |_ -> anomaly (Pp.str "unexpected global_reference in pattern")) ref in + let cstr = match ref with + | ConstructRef cstr -> cstr + | IndRef _ -> + let error = str "There is an inductive name deep in a \"in\" clause." in + user_err_loc (loc, "find_constructor", error) + | ConstRef _ | VarRef _ -> + let error = str "This reference is not a constructor." in + user_err_loc (loc, "find_constructor", error) + in cstr, (function (ind,_ as c) -> match add_params with |Some nb_args -> let nb = -- cgit v1.2.3