diff options
| author |  Julien Forest <julien.forest@ensiie.fr> | 2014-09-22 15:10:56 +0200 |
|---|---|---|
| committer | Julien Forest <julien.forest@ensiie.fr> | 2014-09-22 15:10:56 +0200 |
| commit | 85355cfda7a01fa532f111ee7c4d522a8be8a399 (patch) | |
| tree | 6cbc308752391ea4635953ece74de4f125f8d259 | |
| parent | 71a579d3bb053e686a92aec111f847bb61f4d8a8 (diff) | |
Correction of error message (bug 3359)
| -rw-r--r-- | plugins/funind/recdef.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 _ -> |