diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 12 | ||||
| -rw-r--r-- | engine/evd.ml | 2 | ||||
| -rw-r--r-- | engine/proofview.ml | 2 | ||||
| -rw-r--r-- | engine/uState.ml | 2 |
4 files changed, 9 insertions, 9 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index e5ac3792d6..c0485e4e76 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -295,7 +295,7 @@ let decompose_lam_assum sigma c = let decompose_lam_n_assum sigma n c = let open Rel.Declaration in if n < 0 then - error "decompose_lam_n_assum: integer parameter must be positive"; + user_err Pp.(str "decompose_lam_n_assum: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else @@ -303,14 +303,14 @@ let decompose_lam_n_assum sigma n c = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_assum: not enough abstractions" + | c -> user_err Pp.(str "decompose_lam_n_assum: not enough abstractions") in lamdec_rec Context.Rel.empty n c let decompose_lam_n_decls sigma n = let open Rel.Declaration in if n < 0 then - error "decompose_lam_n_decls: integer parameter must be positive"; + user_err Pp.(str "decompose_lam_n_decls: integer parameter must be positive"); let rec lamdec_rec l n c = if Int.equal n 0 then l,c else @@ -318,7 +318,7 @@ let decompose_lam_n_decls sigma n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | c -> error "decompose_lam_n_decls: not enough abstractions" + | c -> user_err Pp.(str "decompose_lam_n_decls: not enough abstractions") in lamdec_rec Context.Rel.empty n @@ -363,7 +363,7 @@ let decompose_prod_assum sigma c = let decompose_prod_n_assum sigma n c = let open Rel.Declaration in if n < 0 then - error "decompose_prod_n_assum: integer parameter must be positive"; + user_err Pp.(str "decompose_prod_n_assum: integer parameter must be positive"); let rec prodec_rec l n c = if Int.equal n 0 then l,c else @@ -371,7 +371,7 @@ let decompose_prod_n_assum sigma n c = | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | c -> error "decompose_prod_n_assum: not enough assumptions" + | c -> user_err Pp.(str "decompose_prod_n_assum: not enough assumptions") in prodec_rec Context.Rel.empty n c diff --git a/engine/evd.ml b/engine/evd.ml index 8ade6cb996..b677705bc9 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -952,7 +952,7 @@ let declare_principal_goal evk evd = | None -> { evd with future_goals = evk::evd.future_goals; principal_future_goal=Some evk; } - | Some _ -> CErrors.error "Only one main subgoal per instantiation." + | Some _ -> CErrors.user_err Pp.(str "Only one main subgoal per instantiation.") let future_goals evd = evd.future_goals diff --git a/engine/proofview.ml b/engine/proofview.ml index 7f80d40d64..ddfc0e39dd 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -289,7 +289,7 @@ let tclONCE = Proof.once exception MoreThanOneSuccess let _ = CErrors.register_handler begin function - | MoreThanOneSuccess -> CErrors.error "This tactic has more than one success." + | MoreThanOneSuccess -> CErrors.user_err Pp.(str "This tactic has more than one success.") | _ -> raise CErrors.Unhandled end diff --git a/engine/uState.ml b/engine/uState.ml index dc68220575..acef901432 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -188,7 +188,7 @@ let process_universe_constraints ctx cstrs = | _ -> local else begin match Univ.Universe.level r with - | None -> error ("Algebraic universe on the right") + | None -> user_err Pp.(str "Algebraic universe on the right") | Some r' -> if Univ.Level.is_small r' then let levels = Univ.Universe.levels l in |