diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-11-23 11:56:30 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2013-11-23 11:57:01 +0100 |
| commit | 2350a6042b08d3793dc2fac535fadfaa623ac549 (patch) | |
| tree | 2b06e853f8d661089fd6601f65bc63b3e8e36013 | |
| parent | 34ed0bb1b198ff92436177b303e2e6b4db931816 (diff) | |
Fixing bug #3165.
| -rw-r--r-- | interp/constrintern.ml | 12 |
1 files 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 = |