aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml12
-rw-r--r--plugins/funind/functional_principles_types.ml10
-rw-r--r--plugins/funind/g_indfun.ml44
-rw-r--r--plugins/funind/glob_term_to_relation.ml6
-rw-r--r--plugins/funind/glob_termops.ml10
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--plugins/funind/indfun_common.ml4
-rw-r--r--plugins/funind/invfun.ml5
-rw-r--r--plugins/funind/merge.ml2
-rw-r--r--plugins/funind/recdef.ml12
10 files changed, 35 insertions, 32 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 55d361e3d2..64f7813a32 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -820,10 +820,10 @@ let build_proof
build_proof new_finalize {dyn_infos with info = f } g
end
| Fix _ | CoFix _ ->
- error ( "Anonymous local (co)fixpoints are not handled yet")
+ user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet"))
- | Proj _ -> error "Prod"
- | Prod _ -> error "Prod"
+ | Proj _ -> user_err Pp.(str "Prod")
+ | Prod _ -> user_err Pp.(str "Prod")
| LetIn _ ->
let new_infos =
{ dyn_infos with
@@ -1097,7 +1097,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
(Global.env ())
(Evd.empty)
(EConstr.of_constr body)
- | None -> error ( "Cannot define a principle over an axiom ")
+ | None -> user_err Pp.(str "Cannot define a principle over an axiom ")
in
let fbody = get_body fnames.(fun_num) in
let f_ctxt,f_body = decompose_lam (project g) fbody in
@@ -1199,7 +1199,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
bs.(num),
List.rev_map var_of_decl princ_params))
),num
- | _ -> error "Not a mutual block"
+ | _ -> user_err Pp.(str "Not a mutual block")
in
let info =
{infos with
@@ -1594,7 +1594,7 @@ let prove_principle_for_gen
let args_ids = List.map (get_name %> Nameops.out_name) princ_info.args in
let lemma =
match !tcc_lemma_ref with
- | Undefined -> error "No tcc proof !!"
+ | Undefined -> user_err Pp.(str "No tcc proof !!")
| Value lemma -> EConstr.of_constr lemma
| Not_needed -> EConstr.of_constr (Coqlib.build_coq_I ())
in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 529b91c4ca..18d63dd94b 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -75,7 +75,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
let rel_as_kn =
fst (match princ_type_info.indref with
| Some (Globnames.IndRef ind) -> ind
- | _ -> error "Not a valid predicate"
+ | _ -> user_err Pp.(str "Not a valid predicate")
)
in
let ptes_vars = List.map Context.Named.Declaration.get_id new_predicates in
@@ -416,7 +416,7 @@ let get_funs_constant mp dp =
in
let body = EConstr.Unsafe.to_constr body in
body
- | None -> error ( "Cannot define a principle over an axiom ")
+ | None -> user_err Pp.(str ( "Cannot define a principle over an axiom "))
in
let f = find_constant_body const in
let l_const = get_funs_constant const f in
@@ -432,7 +432,7 @@ let get_funs_constant mp dp =
List.iter
(fun params ->
if not (List.equal (fun (n1, c1) (n2, c2) -> Name.equal n1 n2 && eq_constr c1 c2) first_params params)
- then error "Not a mutal recursive block"
+ then user_err Pp.(str "Not a mutal recursive block")
)
l_params
in
@@ -445,7 +445,7 @@ let get_funs_constant mp dp =
| _ ->
if is_first && Int.equal (List.length l_bodies) 1
then raise Not_Rec
- else error "Not a mutal recursive block"
+ else user_err Pp.(str "Not a mutal recursive block")
in
let first_infos = extract_info true (List.hd l_bodies) in
let check body = (* Hope this is correct *)
@@ -454,7 +454,7 @@ let get_funs_constant mp dp =
Array.equal eq_constr ta1 ta2 && Array.equal eq_constr ca1 ca2
in
if not (eq_infos first_infos (extract_info false body))
- then error "Not a mutal recursive block"
+ then user_err Pp.(str "Not a mutal recursive block")
in
List.iter check l_bodies
with Not_Rec -> ()
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 5e6128b1b9..1db8be0818 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -90,7 +90,7 @@ let pr_intro_as_pat _prc _ _ pat =
let out_disjunctive = function
| loc, IntroAction (IntroOrAndPattern l) -> (loc,l)
- | _ -> CErrors.error "Disjunctive or conjunctive intro pattern expected."
+ | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected.")
ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ]
@@ -228,7 +228,7 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
;
try Functional_principles_types.build_scheme fas
with Functional_principles_types.No_graph_found ->
- CErrors.error ("Cannot generate induction principle(s)")
+ CErrors.user_err Pp.(str "Cannot generate induction principle(s)")
| e when CErrors.noncritical e ->
let names = List.map (fun (_,na,_) -> na) fas in
warning_error names e
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 7f2b21e79d..d8614f376d 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -576,8 +576,8 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
WARNING: We need to restart since [b] itself should be an application term
*)
build_entry_lc env funnames avoid (mkGApp(b,args))
- | GRec _ -> error "Not handled GRec"
- | GProd _ -> error "Cannot apply a type"
+ | GRec _ -> user_err Pp.(str "Not handled GRec")
+ | GProd _ -> user_err Pp.(str "Cannot apply a type")
end (* end of the application treatement *)
| GLambda(n,_,t,b) ->
@@ -678,7 +678,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
build_entry_lc env funnames avoid match_expr
end
- | GRec _ -> error "Not handled GRec"
+ | GRec _ -> user_err Pp.(str "Not handled GRec")
| GCast(b,_) ->
build_entry_lc env funnames avoid b
and build_entry_lc_from_case env funname make_discr
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 5abcb100f7..0361e8cb13 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -120,7 +120,7 @@ let remove_name_from_mapping mapping na =
let change_vars =
let rec change_vars mapping rt =
- CAst.map (function
+ CAst.map_with_loc (fun ?loc -> function
| GRef _ as x -> x
| GVar id ->
let new_id =
@@ -172,7 +172,7 @@ let change_vars =
change_vars mapping lhs,
change_vars mapping rhs
)
- | GRec _ -> error "Local (co)fixes are not supported"
+ | GRec _ -> user_err ?loc Pp.(str "Local (co)fixes are not supported")
| GSort _ as x -> x
| GHole _ as x -> x
| GCast(b,c) ->
@@ -352,7 +352,7 @@ let rec alpha_rt excluded rt =
alpha_rt excluded lhs,
alpha_rt excluded rhs
)
- | GRec _ -> error "Not handled GRec"
+ | GRec _ -> user_err Pp.(str "Not handled GRec")
| GSort _
| GHole _ as rt -> rt
| GCast (b,c) ->
@@ -408,7 +408,7 @@ let is_free_in id =
| GIf(cond,_,br1,br2) ->
is_free_in cond || is_free_in br1 || is_free_in br2
- | GRec _ -> raise (UserError(None,str "Not handled GRec"))
+ | GRec _ -> user_err Pp.(str "Not handled GRec")
| GSort _ -> false
| GHole _ -> false
| GCast (b,(CastConv t|CastVM t|CastNative t)) -> is_free_in b || is_free_in t
@@ -695,7 +695,7 @@ let expand_as =
| GIf(e,(na,po),br1,br2) ->
GIf(expand_as map e,(na,Option.map (expand_as map) po),
expand_as map br1, expand_as map br2)
- | GRec _ -> error "Not handled GRec"
+ | GRec _ -> user_err Pp.(str "Not handled GRec")
| GCast(b,c) ->
GCast(expand_as map b,
Miscops.map_cast_type (expand_as map) c)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index ab83cb15a6..74c0eb4cc7 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -186,6 +186,8 @@ let build_newrecursive l =
in
build_newrecursive l'
+let error msg = user_err Pp.(str msg)
+
(* Checks whether or not the mutual bloc is recursive *)
let is_rec names =
let names = List.fold_right Id.Set.add names Id.Set.empty in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index ea985ddecd..91dac303a7 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
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 8c972cd7cf..8747efc02b 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -197,7 +197,7 @@ let generate_type evd g_to_f f graph i =
let find_induction_principle evd f =
let f_as_constant,u = match EConstr.kind !evd f with
| Const c' -> c'
- | _ -> error "Must be used with a function"
+ | _ -> user_err Pp.(str "Must be used with a function")
in
let infos = find_Function_infos f_as_constant in
match infos.rect_lemma with
@@ -701,7 +701,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
let graph_def = graphs.(j) in
let infos =
try find_Function_infos (fst (destConst (project g) funcs.(j)))
- with Not_found -> error "No graph found"
+ with Not_found -> user_err Pp.(str "No graph found")
in
if infos.is_general
|| Rtree.is_infinite Declareops.eq_recarg graph_def.mind_recargs
@@ -1006,6 +1006,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
| _ -> tclFAIL 1 (mt ()) g
+let error msg = user_err Pp.(str msg)
let invfun qhyp f =
let f =
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index b99a05dfbc..b2c8489ce1 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -347,7 +347,7 @@ let filter_shift_stable_right (lnk:int merged_arg array) (l:'a list): 'a list =
filter_shift_stable lnk (Array.to_list larr)
-
+let error msg = user_err Pp.(str msg)
(** {1 Utilities for merging} *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index c463093553..e206955acb 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -136,7 +136,7 @@ let ex = function () -> (coq_init_constant "ex")
let nat = function () -> (coq_init_constant "nat")
let iter_ref () =
try find_reference ["Recdef"] "iter"
- with Not_found -> error "module Recdef not loaded"
+ with Not_found -> user_err Pp.(str "module Recdef not loaded")
let iter = function () -> (constr_of_global (delayed_force iter_ref))
let eq = function () -> (coq_init_constant "eq")
let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
@@ -323,8 +323,8 @@ let check_not_nested sigma forbidden e =
| Construct _ -> ()
| Case(_,t,e,a) ->
check_not_nested t;check_not_nested e;Array.iter check_not_nested a
- | Fix _ -> error "check_not_nested : Fix"
- | CoFix _ -> error "check_not_nested : Fix"
+ | Fix _ -> user_err Pp.(str "check_not_nested : Fix")
+ | CoFix _ -> user_err Pp.(str "check_not_nested : Fix")
in
try
check_not_nested e
@@ -430,8 +430,8 @@ let treat_case forbid_new_ids to_intros finalize_tac nb_lam e infos : tactic =
let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g =
let sigma = project g in
match EConstr.kind sigma expr_info.info with
- | CoFix _ | Fix _ -> error "Function cannot treat local fixpoint or cofixpoint"
- | Proj _ -> error "Function cannot treat projections"
+ | CoFix _ | Fix _ -> user_err Pp.(str "Function cannot treat local fixpoint or cofixpoint")
+ | Proj _ -> user_err Pp.(str "Function cannot treat projections")
| LetIn(na,b,t,e) ->
begin
let new_continuation_tac =
@@ -1304,7 +1304,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
in
let na = next_global_ident_away name [] in
if Termops.occur_existential sigma gls_type then
- CErrors.error "\"abstract\" cannot handle existentials";
+ CErrors.user_err Pp.(str "\"abstract\" cannot handle existentials");
let hook _ _ =
let opacity =
let na_ref = Libnames.Ident (Loc.tag na) in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:33:54 +0000