aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml1
-rw-r--r--pretyping/constr_matching.ml4
-rw-r--r--pretyping/evarconv.ml37
-rw-r--r--pretyping/evarconv.mli2
-rw-r--r--pretyping/evarsolve.ml4
-rw-r--r--pretyping/inductiveops.ml2
-rw-r--r--pretyping/locusops.ml4
-rw-r--r--pretyping/nativenorm.ml2
-rw-r--r--pretyping/patternops.ml2
-rw-r--r--pretyping/program.ml19
-rw-r--r--pretyping/redops.ml8
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/tacred.ml10
-rw-r--r--pretyping/typeclasses.ml2
-rw-r--r--pretyping/unification.ml14
-rw-r--r--pretyping/vnorm.ml2
16 files changed, 64 insertions, 53 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e7b17991e3..c2c8065a98 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -961,7 +961,6 @@ let expand_arg tms (p,ccl) ((_,t),_,na) =
let k = length_of_tomatch_type_sign na t in
(p+k,liftn_predicate (k-1) (p+1) ccl tms)
-
let use_unit_judge evd =
let j, ctx = coq_unit_judge () in
let evd' = Evd.merge_context_set Evd.univ_flexible_alg evd ctx in
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index edcfa99c86..2cb837ba03 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -220,9 +220,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
| PSoApp (n,args),m ->
let fold (ans, seen) = function
| PRel n ->
- let () = if Int.Set.mem n seen then error "Non linear second-order pattern" in
+ let () = if Int.Set.mem n seen then user_err (str "Non linear second-order pattern") in
(n :: ans, Int.Set.add n seen)
- | _ -> error "Only bound indices allowed in second order pattern matching."
+ | _ -> user_err (str "Only bound indices allowed in second order pattern matching.")
in
let relargs, relset = List.fold_left fold ([], Int.Set.empty) args in
let frels = free_rels sigma cT in
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 42aaf3a227..bf62cea6b6 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -42,6 +42,31 @@ let _ = Goptions.declare_bool_option {
Goptions.optwrite = (fun a -> debug_unification:=a);
}
+(*******************************************)
+(* Functions to deal with impossible cases *)
+(*******************************************)
+(* XXX: we would like to search for this with late binding
+ "data.id.type" etc... *)
+let impossible_default_case () =
+ let c, ctx = Universes.fresh_global_instance (Global.env()) (Globnames.ConstRef Coqlib.id) in
+ let (_, u) = Term.destConst c in
+ Some (c, Term.mkConstU (Coqlib.type_of_id, u), ctx)
+
+let coq_unit_judge =
+ let open Environ in
+ let make_judge c t = make_judge (EConstr.of_constr c) (EConstr.of_constr t) in
+ let na1 = Name (Id.of_string "A") in
+ let na2 = Name (Id.of_string "H") in
+ fun () ->
+ match impossible_default_case () with
+ | Some (id, type_of_id, ctx) ->
+ make_judge id type_of_id, ctx
+ | None ->
+ (* In case the constants id/ID are not defined *)
+ Environ.make_judge (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1)))
+ (mkProd (na1,mkProp,mkArrow (mkRel 1) (mkRel 2))),
+ Univ.ContextSet.empty
+
let unfold_projection env evd ts p c =
let cst = Projection.constant p in
if is_transparent_constant ts cst then
@@ -351,7 +376,7 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
match ground_test with
| Some result -> result
| None ->
- (* Until pattern-unification is used consistently, use nohdbeta to not
+ (* Until pattern-unification is used consistently, use nohdbeta to not
destroy beta-redexes that can be used for 1st-order unification *)
let term1 = apprec_nohdbeta (fst ts) env evd term1 in
let term2 = apprec_nohdbeta (fst ts) env evd term2 in
@@ -1051,7 +1076,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
| decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c ->
begin match occs with
| Some _ ->
- error "Cannot force abstraction on identity instance."
+ user_err Pp.(str "Cannot force abstraction on identity instance.")
| None ->
make_subst (ctxt',l,occsl)
end
@@ -1070,7 +1095,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
let set_var k =
match occs with
| Some Locus.AllOccurrences -> mkVar id
- | Some _ -> error "Selection of specific occurrences not supported"
+ | Some _ -> user_err Pp.(str "Selection of specific occurrences not supported")
| None ->
let evty = set_holes evdref cty subst in
let instance = Filter.filter_list filter instance in
@@ -1108,10 +1133,10 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
(* This is an arbitrary choice *)
let evd = Evd.define evk (Constr.mkVar id) evd in
match evar_conv_x ts env_evar evd CUMUL idty evty with
- | UnifFailure _ -> error "Cannot find an instance"
+ | UnifFailure _ -> user_err Pp.(str "Cannot find an instance")
| Success evd ->
match reconsider_unif_constraints (evar_conv_x ts) evd with
- | UnifFailure _ -> error "Cannot find an instance"
+ | UnifFailure _ -> user_err Pp.(str "Cannot find an instance")
| Success evd ->
evd
else
@@ -1245,7 +1270,7 @@ let rec solve_unconstrained_evars_with_candidates ts evd =
| None -> evd
| Some (evk,ev_info,l) ->
let rec aux = function
- | [] -> error "Unsolvable existential variables."
+ | [] -> user_err Pp.(str "Unsolvable existential variables.")
| a::l ->
try
let conv_algo = evar_conv_x ts in
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 7cee1e8a7e..45857df2ae 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -80,3 +80,5 @@ val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool ->
Evarsolve.unification_result
(**/**)
+(** {6 Functions to deal with impossible cases } *)
+val coq_unit_judge : unit -> EConstr.unsafe_judgment Univ.in_universe_context_set
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 4ada91eb59..98e71c7fd9 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1050,7 +1050,7 @@ let do_restrict_hyps evd (evk,args as ev) filter candidates =
| None -> None,candidates
| Some filter -> restrict_hyps evd evk filter candidates in
match candidates,filter with
- | UpdateWith [], _ -> error "Not solvable."
+ | UpdateWith [], _ -> user_err Pp.(str "Not solvable.")
| UpdateWith [nc],_ ->
let evd = Evd.define evk (EConstr.Unsafe.to_constr nc) evd in
raise (EvarSolvedWhileRestricting (evd,mkEvar ev))
@@ -1230,7 +1230,7 @@ let check_evar_instance evd evk1 body conv_algo =
(* This happens in practice, cf MathClasses build failure on 2013-3-15 *)
let ty =
try Retyping.get_type_of ~lax:true evenv evd body
- with Retyping.RetypeError _ -> error "Ill-typed evar instance"
+ with Retyping.RetypeError _ -> user_err Pp.(str "Ill-typed evar instance")
in
match conv_algo evenv evd Reduction.CUMUL ty (EConstr.of_constr evi.evar_concl) with
| Success evd -> evd
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 429e5005ec..7f3bafc685 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -97,7 +97,7 @@ let mis_nf_constructor_type ((ind,u),mib,mip) j =
and ntypes = mib.mind_ntypes
and nconstr = Array.length mip.mind_consnames in
let make_Ik k = mkIndU (((fst ind),ntypes-k-1),u) in
- if j > nconstr then error "Not enough constructors in the type.";
+ if j > nconstr then user_err Pp.(str "Not enough constructors in the type.");
substl (List.init ntypes make_Ik) (subst_instance_constr u specif.(j-1))
(* Number of constructors *)
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index e4fbf8d542..211ffbe01e 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -50,9 +50,9 @@ let is_nowhere = function
let simple_clause_of enum_hyps cl =
let error_occurrences () =
- CErrors.error "This tactic does not support occurrences selection" in
+ CErrors.user_err Pp.(str "This tactic does not support occurrences selection") in
let error_body_selection () =
- CErrors.error "This tactic does not support body selection" in
+ CErrors.user_err Pp.(str "This tactic does not support body selection") in
let hyps =
match cl.onhyps with
| None ->
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 0228f63cdc..afaa20b6f6 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -383,7 +383,7 @@ let native_norm env sigma c ty =
let c = EConstr.Unsafe.to_constr c in
let ty = EConstr.Unsafe.to_constr ty in
if Coq_config.no_native_compiler then
- error "Native_compute reduction has been disabled at configure time."
+ user_err Pp.(str "Native_compute reduction has been disabled at configure time.")
else
let penv = Environ.pre_env env in
(*
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index a8012d35f8..1c8ad0cddd 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -230,7 +230,7 @@ let instantiate_pattern env sigma lvar c =
error_instantiate_pattern id (List.subtract Id.equal ctx vars)
with Not_found (* Map.find failed *) ->
x)
- | (PFix _ | PCoFix _) -> error ("Non instantiable pattern.")
+ | (PFix _ | PCoFix _) -> user_err Pp.(str "Non instantiable pattern.")
| c ->
map_pattern_with_binders (fun id vars -> id::vars) aux vars c in
aux [] c
diff --git a/pretyping/program.ml b/pretyping/program.ml
index de485dbe84..8769c5659e 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -6,26 +6,11 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Pp
open CErrors
open Util
-open Names
-let make_dir l = DirPath.make (List.rev_map Id.of_string l)
-
-let find_reference locstr dir s =
- let dp = make_dir dir in
- let sp = Libnames.make_path dp (Id.of_string s) in
- try Nametab.global_of_path sp
- with Not_found ->
- user_err (str "Library " ++ Libnames.pr_dirpath dp ++
- str " has to be required first.")
-
-let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
-let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s)
-
-let init_constant dir s () = coq_constant "Program" dir s
-let init_reference dir s () = coq_reference "Program" dir s
+let init_constant dir s () = Universes.constr_of_global @@ Coqlib.coq_reference "Program" dir s
+let init_reference dir s () = Coqlib.coq_reference "Program" dir s
let papp evdref r args =
let open EConstr in
diff --git a/pretyping/redops.ml b/pretyping/redops.ml
index 7d65925e57..8e190f40b9 100644
--- a/pretyping/redops.ml
+++ b/pretyping/redops.ml
@@ -20,13 +20,13 @@ let make_red_flag l =
| FZeta :: lf -> add_flag { red with rZeta = true } lf
| FConst l :: lf ->
if red.rDelta then
- CErrors.error
- "Cannot set both constants to unfold and constants not to unfold";
+ CErrors.user_err Pp.(str
+ "Cannot set both constants to unfold and constants not to unfold");
add_flag { red with rConst = union_consts red.rConst l } lf
| FDeltaBut l :: lf ->
if red.rConst <> [] && not red.rDelta then
- CErrors.error
- "Cannot set both constants to unfold and constants not to unfold";
+ CErrors.user_err Pp.(str
+ "Cannot set both constants to unfold and constants not to unfold");
add_flag
{ red with rConst = union_consts red.rConst l; rDelta = true }
lf
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 117ed338ee..e7c9635829 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1219,7 +1219,7 @@ let clos_norm_flags flgs env sigma t =
EConstr.of_constr (CClosure.norm_val
(CClosure.create_clos_infos ~evars flgs env)
(CClosure.inject (EConstr.Unsafe.to_constr t)))
- with e when is_anomaly e -> error "Tried to normalize ill-typed term"
+ with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
let clos_whd_flags flgs env sigma t =
try
@@ -1227,7 +1227,7 @@ let clos_whd_flags flgs env sigma t =
EConstr.of_constr (CClosure.whd_val
(CClosure.create_clos_infos ~evars flgs env)
(CClosure.inject (EConstr.Unsafe.to_constr t)))
- with e when is_anomaly e -> error "Tried to normalize ill-typed term"
+ with e when is_anomaly e -> user_err Pp.(str "Tried to normalize ill-typed term")
let nf_beta = clos_norm_flags CClosure.beta (Global.env ())
let nf_betaiota = clos_norm_flags CClosure.betaiota (Global.env ())
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 67221046bd..3d41d2ddd5 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -858,7 +858,7 @@ let try_red_product env sigma c =
let red_product env sigma c =
try try_red_product env sigma c
- with Redelimination -> error "No head constant to reduce."
+ with Redelimination -> user_err (str "No head constant to reduce.")
(*
(* This old version of hnf uses betadeltaiota instead of itself (resp
@@ -1080,7 +1080,7 @@ let unfold env sigma name c =
if is_evaluable env name then
clos_norm_flags (unfold_red name) env sigma c
else
- error (string_of_evaluable_ref env name^" is opaque.")
+ user_err Pp.(str (string_of_evaluable_ref env name^" is opaque."))
(* [unfoldoccs : (readable_constraints -> (int list * full_path) -> constr -> constr)]
* Unfolds the constant name in a term c following a list of occurrences occl.
@@ -1090,7 +1090,7 @@ let unfoldoccs env sigma (occs,name) c =
let unfo nowhere_except_in locs =
let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in
if Int.equal nbocc 1 then
- error ((string_of_evaluable_ref env name)^" does not occur.");
+ user_err Pp.(str ((string_of_evaluable_ref env name)^" does not occur."));
let rest = List.filter (fun o -> o >= nbocc) locs in
let () = match rest with
| [] -> ()
@@ -1112,7 +1112,7 @@ let unfoldn loccname env sigma c =
let fold_one_com com env sigma c =
let rcom =
try red_product env sigma com
- with Redelimination -> error "Not reducible." in
+ with Redelimination -> user_err Pp.(str "Not reducible.") in
(* Reason first on the beta-iota-zeta normal form of the constant as
unfold produces it, so that the "unfold f; fold f" configuration works
to refold fix expressions *)
@@ -1147,7 +1147,7 @@ let compute = cbv_betadeltaiota
let abstract_scheme env sigma (locc,a) (c, sigma) =
let ta = Retyping.get_type_of env sigma a in
let na = named_hd env sigma ta Anonymous in
- if occur_meta sigma ta then error "Cannot find a type for the generalisation.";
+ if occur_meta sigma ta then user_err Pp.(str "Cannot find a type for the generalisation.");
if occur_meta sigma a then
mkLambda (na,ta,c), sigma
else
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 919e95a8ee..d7b4842810 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -422,7 +422,7 @@ let add_class cl =
match inst with
| Some (Backward, info) ->
(match body with
- | None -> CErrors.error "Non-definable projection can not be declared as a subinstance"
+ | None -> CErrors.user_err Pp.(str "Non-definable projection can not be declared as a subinstance")
| Some b -> declare_instance (Some info) false (ConstRef b))
| _ -> ())
cl.cl_projs
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index cac6c50572..d1643a8c7d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1250,7 +1250,7 @@ let applyHead env (type r) (evd : r Sigma.t) n c =
| Prod (_,c1,c2) ->
let Sigma (evar, evd', q) = Evarutil.new_evar env evd ~src:(Loc.tag Evar_kinds.GoalEvar) c1 in
apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) (p +> q) evd'
- | _ -> error "Apply_Head_Then"
+ | _ -> user_err Pp.(str "Apply_Head_Then")
in
apprec n c (Typing.unsafe_type_of env (Sigma.to_evar_map evd) c) Sigma.refl evd
@@ -1516,7 +1516,7 @@ let w_typed_unify_array env evd flags f1 l1 f2 l2 =
let iter_fail f a =
let n = Array.length a in
let rec ffail i =
- if Int.equal i n then error "iter_fail"
+ if Int.equal i n then user_err Pp.(str "iter_fail")
else
try f a.(i)
with ex when precatchable_exception ex -> ffail (i+1)
@@ -1754,8 +1754,8 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
w_typed_unify_array env evd flags f1 l1 f2 l2,cl
else w_typed_unify env evd CONV flags op cl,cl
with ex when Pretype_errors.unsatisfiable_exception ex ->
- bestexn := Some ex; error "Unsat")
- else error "Bound 1"
+ bestexn := Some ex; user_err Pp.(str "Unsat"))
+ else user_err Pp.(str "Bound 1")
with ex when precatchable_exception ex ->
(match EConstr.kind evd cl with
| App (f,args) ->
@@ -1804,7 +1804,7 @@ let w_unify_to_subterm env evd ?(flags=default_unify_flags ()) (op,cl) =
with ex when precatchable_exception ex ->
matchrec c)
- | _ -> error "Match_subterm"))
+ | _ -> user_err Pp.(str "Match_subterm")))
in
try matchrec cl
with ex when precatchable_exception ex ->
@@ -1820,7 +1820,7 @@ let w_unify_to_subterm_all env evd ?(flags=default_unify_flags ()) (op,cl) =
let (evd,c as a) = a () in
if List.exists (fun (evd',c') -> EConstr.eq_constr evd' c c') b then b else a :: b
in
- let fail str _ = error str in
+ let fail str _ = user_err (Pp.str str) in
let bind f g a =
let a1 = try f a
with ex
@@ -1956,7 +1956,7 @@ let w_unify2 env evd flags dep cv_pb ty1 ty2 =
| _, Meta p2 ->
(* Find the predicate *)
secondOrderAbstractionAlgo dep env evd flags ty1 (p2, oplist2)
- | _ -> error "w_unify2"
+ | _ -> user_err Pp.(str "w_unify2")
(* The unique unification algorithm works like this: If the pattern is
flexible, and the goal has a lambda-abstraction at the head, then
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 74998349be..b08666483e 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -355,7 +355,7 @@ and nf_cofix env sigma cf =
let cbv_vm env sigma c t =
if Termops.occur_meta_or_existential sigma c then
- CErrors.error "vm_compute does not support existential variables.";
+ CErrors.user_err Pp.(str "vm_compute does not support existential variables.");
(** This evar-normalizes terms beforehand *)
let c = EConstr.to_constr sigma c in
let t = EConstr.to_constr sigma t in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 06:25:00 +0000