aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/checker.ml2
-rwxr-xr-xdev/tools/backport-pr.sh9
-rw-r--r--engine/logic_monad.ml1
-rw-r--r--engine/logic_monad.mli1
-rw-r--r--kernel/reduction.ml12
-rw-r--r--kernel/reduction.mli6
-rw-r--r--kernel/term.ml6
-rw-r--r--kernel/term.mli12
-rw-r--r--lib/coqProject_file.ml42
-rw-r--r--lib/feedback.mli5
-rw-r--r--pretyping/vnorm.ml3
-rw-r--r--printing/printmod.ml10
-rw-r--r--stm/stm.ml28
-rw-r--r--test-suite/output/Inductive.out4
-rw-r--r--test-suite/output/Inductive.v4
-rw-r--r--tools/coqdep.ml2
-rw-r--r--toplevel/coqloop.ml4
-rw-r--r--vernac/vernacentries.ml4
18 files changed, 77 insertions, 38 deletions
diff --git a/checker/checker.ml b/checker/checker.ml
index b8b4d5dc2c..e8eff889c8 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -18,7 +18,7 @@ let () = at_exit flush_all
let chk_pp = Pp.pp_with Format.std_formatter
let fatal_error info anomaly =
- flush_all (); Feedback.msg_error info; flush_all ();
+ flush_all (); Format.eprintf "@[Fatal Error: @[%a@]@]%!@\n" Pp.pp_with info; flush_all ();
exit (if anomaly then 129 else 1)
let coq_root = Id.of_string "Coq"
diff --git a/dev/tools/backport-pr.sh b/dev/tools/backport-pr.sh
index d7acf01f1d..e4359f7038 100755
--- a/dev/tools/backport-pr.sh
+++ b/dev/tools/backport-pr.sh
@@ -50,6 +50,15 @@ else
fi
+if ! git diff --exit-code HEAD ${BRANCH} -- "*.mli"; then
+ echo
+ read -p "Some mli files are modified. Bypass? [y/N] " -n 1 -r
+ echo
+ if [[ ! $REPLY =~ ^[Yy]$ ]]; then
+ exit 1
+ fi
+fi
+
if [[ "${OPTION}" == "--stop-before-merging" ]]; then
exit 0
fi
diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 9dc5d473b9..3674bb9432 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -107,7 +107,6 @@ struct
let print_debug s = make (fun _ -> Feedback.msg_info s)
let print_info s = make (fun _ -> Feedback.msg_info s)
let print_warning s = make (fun _ -> Feedback.msg_warning s)
- let print_error s = make (fun _ -> Feedback.msg_error s)
let print_notice s = make (fun _ -> Feedback.msg_notice s)
let run = fun x ->
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 8c8f9fe935..50b4abd8bd 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -61,7 +61,6 @@ module NonLogical : sig
val print_warning : Pp.t -> unit t
val print_notice : Pp.t -> unit t
val print_info : Pp.t -> unit t
- val print_error : Pp.t -> unit t
(** [Pervasives.raise]. Except that exceptions are wrapped with
{!Exception}. *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 159d2ea665..da7042713f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -882,6 +882,18 @@ let hnf_prod_app env t n =
let hnf_prod_applist env t nl =
List.fold_left (hnf_prod_app env) t nl
+let hnf_prod_applist_assum env n c l =
+ let rec app n subst t l =
+ if Int.equal n 0 then
+ if l == [] then substl subst t
+ else anomaly (Pp.str "Too many arguments.")
+ else match kind (whd_allnolet env t), l with
+ | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l
+ | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+ | _, [] -> anomaly (Pp.str "Not enough arguments.")
+ | _ -> anomaly (Pp.str "Not enough prod/let's.") in
+ app n [] c l
+
(* Dealing with arities *)
let dest_prod env =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 0e6a2b8199..6f7e3f8f8f 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -105,6 +105,12 @@ val beta_app : constr -> constr -> constr
(** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *)
val hnf_prod_applist : env -> types -> constr list -> types
+(** In [hnf_prod_applist_assum n c args], [c] is supposed to (whd-)reduce to
+ the form [∀Γ.t] with [Γ] of length [n] and possibly with let-ins; it
+ returns [t] with the assumptions of [Γ] instantiated by [args] and
+ the local definitions of [Γ] expanded. *)
+val hnf_prod_applist_assum : env -> int -> types -> constr list -> types
+
(** Compatibility alias for Term.lambda_appvect_assum *)
val betazeta_appvect : int -> constr -> constr array -> constr
diff --git a/kernel/term.ml b/kernel/term.ml
index fae990d45f..a4c92bd333 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -352,10 +352,11 @@ let lambda_applist_assum n c l =
let rec app n subst t l =
if Int.equal n 0 then
if l == [] then substl subst t
- else anomaly (Pp.str "Not enough arguments.")
+ else anomaly (Pp.str "Too many arguments.")
else match kind_of_term t, l with
| Lambda(_,_,c), arg::l -> app (n-1) (arg::subst) c l
| LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+ | _, [] -> anomaly (Pp.str "Not enough arguments.")
| _ -> anomaly (Pp.str "Not enough lambda/let's.") in
app n [] c l
@@ -377,10 +378,11 @@ let prod_applist_assum n c l =
let rec app n subst t l =
if Int.equal n 0 then
if l == [] then substl subst t
- else anomaly (Pp.str "Not enough arguments.")
+ else anomaly (Pp.str "Too many arguments.")
else match kind_of_term t, l with
| Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l
| LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l
+ | _, [] -> anomaly (Pp.str "Not enough arguments.")
| _ -> anomaly (Pp.str "Not enough prod/let's.") in
app n [] c l
diff --git a/kernel/term.mli b/kernel/term.mli
index c9a8cf6e1e..b4597676a3 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -242,7 +242,7 @@ val lambda_applist : constr -> constr list -> constr
val lambda_appvect : constr -> constr array -> constr
(** In [lambda_applist_assum n c args], [c] is supposed to have the
- form [λΓ.c] with [Γ] of length [m] and possibly with let-ins; it
+ form [λΓ.c] with [Γ] of length [n] and possibly with let-ins; it
returns [c] with the assumptions of [Γ] instantiated by [args] and
the local definitions of [Γ] expanded. *)
val lambda_applist_assum : int -> constr -> constr list -> constr
@@ -251,15 +251,15 @@ val lambda_appvect_assum : int -> constr -> constr array -> constr
(** pseudo-reduction rule *)
(** [prod_appvect] [forall (x1:B1;...;xn:Bn), B] [a1...an] @return [B[a1...an]] *)
-val prod_appvect : constr -> constr array -> constr
-val prod_applist : constr -> constr list -> constr
+val prod_appvect : types -> constr array -> types
+val prod_applist : types -> constr list -> types
(** In [prod_appvect_assum n c args], [c] is supposed to have the
- form [∀Γ.c] with [Γ] of length [m] and possibly with let-ins; it
+ form [∀Γ.c] with [Γ] of length [n] and possibly with let-ins; it
returns [c] with the assumptions of [Γ] instantiated by [args] and
the local definitions of [Γ] expanded. *)
-val prod_appvect_assum : int -> constr -> constr array -> constr
-val prod_applist_assum : int -> constr -> constr list -> constr
+val prod_appvect_assum : int -> types -> constr array -> types
+val prod_applist_assum : int -> types -> constr list -> types
(** {5 Other term destructors. } *)
diff --git a/lib/coqProject_file.ml4 b/lib/coqProject_file.ml4
index 1e52af0be7..e6f1d7e063 100644
--- a/lib/coqProject_file.ml4
+++ b/lib/coqProject_file.ml4
@@ -114,7 +114,7 @@ let process_cmd_line orig_dir proj args =
let parsing_project_file = ref (proj.project_file <> None) in
let orig_dir = (* avoids turning foo.v in ./foo.v *)
if orig_dir = "." then "" else orig_dir in
- let error s = Feedback.msg_error (Pp.str (s^".")); exit 1 in
+ let error s = Format.eprintf "@[%a]@@\n%!" Pp.pp_with Pp.(str (s^".")); exit 1 in
let mk_path d =
let p = CUnix.correct_path d orig_dir in
{ path = CUnix.remove_path_dot (post_canonize p);
diff --git a/lib/feedback.mli b/lib/feedback.mli
index 62b909516f..37f38c8ffd 100644
--- a/lib/feedback.mli
+++ b/lib/feedback.mli
@@ -94,8 +94,9 @@ val msg_warning : ?loc:Loc.t -> Pp.t -> unit
consequences. *)
val msg_error : ?loc:Loc.t -> Pp.t -> unit
-(** Message indicating that something went really wrong, though still
- recoverable; otherwise an exception would have been raised. *)
+[@@ocaml.deprecated "msg_error is an internal function and should not be \
+ used unless you know what you are doing. Use \
+ [CErrors.user_err] instead."]
val msg_debug : ?loc:Loc.t -> Pp.t -> unit
(** For debugging purposes *)
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index b21fbf0eb2..c93b41786b 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -240,8 +240,9 @@ and nf_stk ?from:(from=0) env sigma c t stk =
let (mib,mip) = Inductive.lookup_mind_specif env ind in
let nparams = mib.mind_nparams in
let params,realargs = Util.Array.chop nparams allargs in
+ let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
let pT =
- hnf_prod_applist env (type_of_ind env (ind,u)) (Array.to_list params) in
+ hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in
let pT = whd_all env pT in
let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in
(* Calcul du type des branches *)
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 35487e09c1..2cdb9be3f0 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -93,10 +93,11 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
else Univ.Instance.empty in
let mip = mib.mind_packets.(i) in
let params = Inductive.inductive_paramdecls (mib,u) in
+ let nparamdecls = Context.Rel.length params in
let args = Context.Rel.to_extended_list mkRel 0 params in
- let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
+ let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in
let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
- let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
+ let cstrtypes = Array.map (fun c -> hnf_prod_applist_assum env nparamdecls c args) cstrtypes in
let envpar = push_rel_context params env in
let inst =
if Declareops.inductive_is_polymorphic mib then
@@ -173,10 +174,11 @@ let print_record env mind mib udecl =
in
let mip = mib.mind_packets.(0) in
let params = Inductive.inductive_paramdecls (mib,u) in
+ let nparamdecls = Context.Rel.length params in
let args = Context.Rel.to_extended_list mkRel 0 params in
- let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
+ let arity = hnf_prod_applist_assum env nparamdecls (build_ind_type env ((mib,mip),u)) args in
let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
- let cstrtype = hnf_prod_applist env cstrtypes.(0) args in
+ let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in
let fields = get_fields cstrtype in
let envpar = push_rel_context params env in
let bl = Universes.universe_binders_with_opt_names (IndRef (mind,0))
diff --git a/stm/stm.ml b/stm/stm.ml
index b5848c662c..6c956e1342 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -85,8 +85,7 @@ let stm_purify f x =
Exninfo.iraise e
let execution_error ?loc state_id msg =
- feedback ~id:state_id
- (Message (Error, loc, msg))
+ feedback ~id:state_id (Message (Error, loc, msg))
module Hooks = struct
@@ -1579,12 +1578,13 @@ end = struct (* {{{ *)
| ReqStates sl -> RespStates (perform_states sl)
let on_marshal_error s = function
- | States _ -> msg_error(Pp.strbrk("Marshalling error: "^s^". "^
- "The system state could not be sent to the master process."))
+ | States _ ->
+ msg_warning Pp.(strbrk("Marshalling error: "^s^". "^
+ "The system state could not be sent to the master process."))
| BuildProof { t_exn_info; t_stop; t_assign; t_loc; t_drop = drop_pt } ->
- msg_error(Pp.strbrk("Marshalling error: "^s^". "^
- "The system state could not be sent to the worker process. "^
- "Falling back to local, lazy, evaluation."));
+ msg_warning Pp.(strbrk("Marshalling error: "^s^". "^
+ "The system state could not be sent to the worker process. "^
+ "Falling back to local, lazy, evaluation."));
t_assign(`Comp(build_proof_here ?loc:t_loc ~drop_pt t_exn_info t_stop));
feedback (InProgress ~-1)
@@ -1672,7 +1672,7 @@ end = struct (* {{{ *)
let (e, info) = CErrors.push e in
(try match Stateid.get info with
| None ->
- msg_error Pp.(
+ msg_warning Pp.(
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
spc () ++ iprint (e, info))
| Some (_, cur) ->
@@ -1682,17 +1682,17 @@ end = struct (* {{{ *)
| { step = `Qed ( { qast = { loc } }, _) }
| { step = `Sideff (ReplayCommand { loc }, _) } ->
let start, stop = Option.cata Loc.unloc (0,0) loc in
- msg_error Pp.(
+ msg_warning Pp.(
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
str ": chars " ++ int start ++ str "-" ++ int stop ++
spc () ++ iprint (e, info))
| _ ->
- msg_error Pp.(
+ msg_warning Pp.(
str"File " ++ str name ++ str ": proof of " ++ str r_name ++
spc () ++ iprint (e, info))
with e ->
- msg_error Pp.(str"unable to print error message: " ++
- str (Printexc.to_string e)));
+ msg_warning Pp.(str"unable to print error message: " ++
+ str (Printexc.to_string e)));
if drop then `ERROR_ADMITTED else `ERROR
let finish_task name (u,cst,_) d p l i =
@@ -2429,7 +2429,7 @@ let known_state ?(redefine_qed=false) ~cache id =
| { VCS.kind = `Edit (_,_,_, okeep, _) }, Some (ofp, cancel) ->
assert(redefine_qed = true);
if okeep != keep then
- msg_error(strbrk("The command closing the proof changed. "
+ msg_warning(strbrk("The command closing the proof changed. "
^"The kernel cannot take this into account and will "
^(if keep == VtKeep then "not check " else "reject ")
^"the "^(if keep == VtKeep then "new" else "incomplete")
@@ -2702,7 +2702,7 @@ let finish_tasks name u d p (t,rcbackup as tasks) =
(u,a,true), p
with e ->
let e = CErrors.push e in
- msg_error (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
+ msg_warning (str"File " ++ str name ++ str ":" ++ spc () ++ iprint e);
exit 1
let merge_proof_branch ~valid ?id qast keep brname =
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index e912003f03..af202ea01c 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -1,3 +1,7 @@
The command has indeed failed with message:
Last occurrence of "list'" must have "A" as 1st argument in
"A -> list' A -> list' (A * A)%type".
+Inductive foo (A : Type) (x : A) (y : A := x) : Prop := Foo : foo A x
+
+For foo: Argument scopes are [type_scope _]
+For Foo: Argument scopes are [type_scope _]
diff --git a/test-suite/output/Inductive.v b/test-suite/output/Inductive.v
index 8db8956e32..8ff91268a6 100644
--- a/test-suite/output/Inductive.v
+++ b/test-suite/output/Inductive.v
@@ -1,3 +1,7 @@
Fail Inductive list' (A:Set) : Set :=
| nil' : list' A
| cons' : A -> list' A -> list' (A*A).
+
+(* Check printing of let-ins *)
+Inductive foo (A : Type) (x : A) (y := x) := Foo.
+Print foo.
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 2433cb1d0f..ca14b11bc1 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -539,4 +539,4 @@ let _ =
coqdep ()
with CErrors.UserError(s,p) ->
let pp = (match s with | None -> p | Some s -> Pp.(str s ++ str ": " ++ p)) in
- Feedback.msg_error pp
+ Format.eprintf "%a@\n%!" Pp.pp_with pp
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 5c1b27c333..aade101a45 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -312,7 +312,7 @@ let do_vernac ~time doc sid =
top_stderr (fnl ()); raise CErrors.Quit
| CErrors.Drop -> (* Last chance *)
if Mltop.is_ocaml_top() then raise CErrors.Drop
- else (Feedback.msg_error (str "There is no ML toplevel."); doc, sid)
+ else (Feedback.msg_warning (str "There is no ML toplevel."); doc, sid)
(* Exception printing should be done by the feedback listener,
however this is not yet ready so we rely on the exception for
now. *)
@@ -353,7 +353,7 @@ let rec loop ~time doc =
| CErrors.Drop -> doc
| CErrors.Quit -> exit 0
| any ->
- Feedback.msg_error (str "Anomaly: main loop exited with exception: " ++
+ top_stderr (str "Anomaly: main loop exited with exception: " ++
str (Printexc.to_string any) ++
fnl() ++
str"Please report" ++
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index be09696d1b..7223389c41 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -189,7 +189,7 @@ let print_module r =
Feedback.msg_notice (Printmod.print_module (Printmod.printable_body obj_dir) obj_mp)
| _ -> raise Not_found
with
- Not_found -> Feedback.msg_error (str"Unknown Module " ++ pr_qualid qid)
+ Not_found -> user_err (str"Unknown Module " ++ pr_qualid qid)
let print_modtype r =
let (loc,qid) = qualid_of_reference r in
@@ -202,7 +202,7 @@ let print_modtype r =
let mp = Nametab.locate_module qid in
Feedback.msg_notice (Printmod.print_module false mp)
with Not_found ->
- Feedback.msg_error (str"Unknown Module Type or Module " ++ pr_qualid qid)
+ user_err (str"Unknown Module Type or Module " ++ pr_qualid qid)
let print_namespace ns =
let ns = List.rev (Names.DirPath.repr ns) in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 12:52:30 +0000