diff options
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index ea985ddec..91dac303a 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -502,13 +502,13 @@ let list_rewrite (rev:bool) (eqs: (EConstr.constr*bool) list) = (if rev then (List.rev eqs) else eqs) (tclFAIL 0 (mt())));; let decompose_lam_n sigma n = - if n < 0 then CErrors.error "decompose_lam_n: integer parameter must be positive"; + if n < 0 then CErrors.user_err Pp.(str "decompose_lam_n: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else match EConstr.kind sigma c with | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | _ -> CErrors.error "decompose_lam_n: not enough abstractions" + | _ -> CErrors.user_err Pp.(str "decompose_lam_n: not enough abstractions") in lamdec_rec [] n |