From 85355cfda7a01fa532f111ee7c4d522a8be8a399 Mon Sep 17 00:00:00 2001 From: Julien Forest Date: Mon, 22 Sep 2014 15:10:56 +0200 Subject: Correction of error message (bug 3359) --- plugins/funind/recdef.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index f3096e7a7..9f52258ed 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -462,7 +462,8 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) = jinfo.apP (f,args) expr_info continuation_tac in travel_args jinfo expr_info.is_main_branch new_continuation_tac new_infos - | _ -> assert false + | Case _ -> errorlabstrm "Recdef.travel" (str "the term " ++ Printer.pr_lconstr expr_info.info ++ str " can not contain an applied match (See Limitation in Section 2.3 of refman)") + | _ -> anomaly (Pp.str "travel_aux : unexpected "++ Printer.pr_lconstr expr_info.info) end | Cast(t,_,_) -> travel jinfo continuation_tac {expr_info with info=t} | Const _ | Var _ | Meta _ | Evar _ | Sort _ | Construct _ | Ind _ -> -- cgit v1.2.3