aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CREDITS3
-rw-r--r--doc/changelog/10-standard-library/09379-splitAt.rst5
-rw-r--r--doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst8
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst1
-rw-r--r--interp/notation.ml2
-rw-r--r--interp/syntax_def.ml4
-rw-r--r--plugins/setoid_ring/newring.ml91
-rw-r--r--plugins/setoid_ring/newring_ast.ml6
-rw-r--r--plugins/setoid_ring/newring_ast.mli6
-rw-r--r--stm/stm.ml13
-rw-r--r--test-suite/output/NoAxiomFromR.out1
-rw-r--r--test-suite/output/NoAxiomFromR.v10
-rw-r--r--theories/Init/Datatypes.v13
-rw-r--r--theories/Lists/List.v24
-rw-r--r--theories/Reals/RIneq.v1
-rw-r--r--theories/Vectors/VectorDef.v10
-rw-r--r--theories/Vectors/VectorSpec.v34
-rw-r--r--toplevel/ccompile.ml6
-rw-r--r--toplevel/coqargs.ml19
-rw-r--r--toplevel/coqcargs.ml8
-rw-r--r--toplevel/vernac.ml2
21 files changed, 167 insertions, 100 deletions
diff --git a/CREDITS b/CREDITS
index 989e449cc5..888824aa31 100644
--- a/CREDITS
+++ b/CREDITS
@@ -112,6 +112,7 @@ of the Coq Proof assistant during the indicated time:
Hugo Herbelin (INRIA, 1996-now)
Sébastien Hinderer (INRIA, 2014)
Gérard Huet (INRIA, 1985-1997)
+ Konstantinos Kallas (U. Penn, 2019)
Matej Košík (INRIA, 2015-2017)
Leonidas Lampropoulos (University of Pennsylvania, 2018)
Pierre Letouzey (LRI, 2000-2004, PPS, 2005-2008,
@@ -119,7 +120,7 @@ of the Coq Proof assistant during the indicated time:
Yao Li (ORCID: https://orcid.org/0000-0001-8720-883X,
University of Pennsylvania, 2018)
Yishuai Li (ORCID: https://orcid.org/0000-0002-5728-5903
- U. Penn, 2018)
+ U. Penn, 2018-2019)
Patrick Loiseleur (Paris Sud, 1997-1999)
Evgeny Makarov (INRIA, 2007)
Gregory Malecha (Harvard University 2013-2015,
diff --git a/doc/changelog/10-standard-library/09379-splitAt.rst b/doc/changelog/10-standard-library/09379-splitAt.rst
new file mode 100644
index 0000000000..7ffe8e27f7
--- /dev/null
+++ b/doc/changelog/10-standard-library/09379-splitAt.rst
@@ -0,0 +1,5 @@
+- Added ``splitat`` function and lemmas about ``splitat`` and ``uncons``
+ (`#9379 <https://github.com/coq/coq/pull/9379>`_,
+ by Yishuai Li, with help of Konstantinos Kallas,
+ follow-up of `#8365 <https://github.com/coq/coq/pull/8365>`_,
+ which added ``uncons`` in 8.10+beta1).
diff --git a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst
index f68b2aaaa2..864c4e6a7e 100644
--- a/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst
+++ b/doc/changelog/10-standard-library/10651-new-lemmas-for-lists.rst
@@ -1,4 +1,6 @@
-- New lemmas on :g:`combine`, :g:`filter`, and :g:`nodup` functions on lists. The lemma
- :g:`filter_app` was moved to the :g:`List` module.
+- New lemmas on :g:`combine`, :g:`filter`, :g:`nodup`, :g:`nth`, and
+ :g:`nth_error` functions on lists. The lemma :g:`filter_app` was moved to the
+ :g:`List` module.
- See `#10651 <https://github.com/coq/coq/pull/10651>`_, by Oliver Nash.
+ See `#10651 <https://github.com/coq/coq/pull/10651>`_, and
+ `#10731 <https://github.com/coq/coq/pull/10731>`_, by Oliver Nash.
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index c391cc949d..2885d6dc33 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -627,6 +627,7 @@ file is a particular case of module called *library file*.
as ``Export``.
.. cmdv:: From @dirpath Require @qualid
+ :name: From ... Require ...
This command acts as :cmd:`Require`, but picks
any library whose absolute name is of the form :n:`@dirpath.@dirpath’.@qualid`
diff --git a/interp/notation.ml b/interp/notation.ml
index a78bc60e83..ea2173860d 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -1205,7 +1205,7 @@ let interp_notation ?loc ntn local_scopes =
let scopes = make_current_scopes local_scopes in
try
let (n,sc) = find_interpretation ntn (find_notation ntn) scopes in
- Option.iter (fun d -> warn_deprecated_notation (ntn,d)) n.not_deprecation;
+ Option.iter (fun d -> warn_deprecated_notation ?loc (ntn,d)) n.not_deprecation;
n.not_interp, (n.not_location, sc)
with Not_found ->
user_err ?loc
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 302bb6ece2..9dded8656c 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -100,7 +100,7 @@ let warn_deprecated_syntactic_definition =
let search_syntactic_definition ?loc kn =
let syndef = KNmap.find kn !syntax_table in
let def = out_pat syndef.syndef_pattern in
- Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation;
+ Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
def
let search_filtered_syntactic_definition ?loc filter kn =
@@ -108,5 +108,5 @@ let search_filtered_syntactic_definition ?loc filter kn =
let def = out_pat syndef.syndef_pattern in
let res = filter def in
if Option.has_some res then
- Option.iter (fun d -> warn_deprecated_syntactic_definition (kn,d)) syndef.syndef_deprecation;
+ Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
res
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b456d2eed2..76c393450b 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -18,7 +18,6 @@ open EConstr
open Vars
open CClosure
open Environ
-open Libnames
open Globnames
open Glob_term
open Locus
@@ -326,19 +325,18 @@ let _ = add_map "ring"
module Cmap = Map.Make(Constr)
let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
-let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table"
let print_rings () =
Feedback.msg_notice (strbrk "The following ring structures have been declared:");
- Spmap.iter (fun fn fi ->
+ Cmap.iter (fun _carrier ring ->
let env = Global.env () in
let sigma = Evd.from_env env in
Feedback.msg_notice
(hov 2
- (Ppconstr.pr_id (Libnames.basename fn)++spc()++
- str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++
- str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req))
- ) !from_name
+ (Ppconstr.pr_id ring.ring_name ++ spc() ++
+ str"with carrier "++ pr_constr_env env sigma ring.ring_carrier++spc()++
+ str"and equivalence relation "++ pr_constr_env env sigma ring.ring_req))
+ ) !from_carrier
let ring_for_carrier r = Cmap.find r !from_carrier
@@ -361,9 +359,7 @@ let find_ring_structure env sigma l =
| [] -> assert false
let add_entry (sp,_kn) e =
- from_carrier := Cmap.add e.ring_carrier e !from_carrier;
- from_name := Spmap.add sp e !from_name
-
+ from_carrier := Cmap.add e.ring_carrier e !from_carrier
let subst_th (subst,th) =
let c' = subst_mps subst th.ring_carrier in
@@ -391,7 +387,8 @@ let subst_th (subst,th) =
pretac' == th.ring_pre_tac &&
posttac' == th.ring_post_tac then th
else
- { ring_carrier = c';
+ { ring_name = th.ring_name;
+ ring_carrier = c';
ring_req = eq';
ring_setoid = set';
ring_ext = ext';
@@ -428,59 +425,6 @@ let op_morph r add mul opp req m1 m2 m3 =
let op_smorph r add mul req m1 m2 =
lapp coq_mk_seqe [| r; add; mul; req; m1; m2 |]
-(* let default_ring_equality (r,add,mul,opp,req) = *)
-(* let is_setoid = function *)
-(* {rel_refl=Some _; rel_sym=Some _;rel_trans=Some _;rel_aeq=rel} -> *)
-(* eq_constr_nounivs req rel (\* Qu: use conversion ? *\) *)
-(* | _ -> false in *)
-(* match default_relation_for_carrier ~filter:is_setoid r with *)
-(* Leibniz _ -> *)
-(* let setoid = lapp coq_eq_setoid [|r|] in *)
-(* let op_morph = *)
-(* match opp with *)
-(* Some opp -> lapp coq_eq_morph [|r;add;mul;opp|] *)
-(* | None -> lapp coq_eq_smorph [|r;add;mul|] in *)
-(* (setoid,op_morph) *)
-(* | Relation rel -> *)
-(* let setoid = setoid_of_relation rel in *)
-(* let is_endomorphism = function *)
-(* { args=args } -> List.for_all *)
-(* (function (var,Relation rel) -> *)
-(* var=None && eq_constr_nounivs req rel *)
-(* | _ -> false) args in *)
-(* let add_m = *)
-(* try default_morphism ~filter:is_endomorphism add *)
-(* with Not_found -> *)
-(* error "ring addition should be declared as a morphism" in *)
-(* let mul_m = *)
-(* try default_morphism ~filter:is_endomorphism mul *)
-(* with Not_found -> *)
-(* error "ring multiplication should be declared as a morphism" in *)
-(* let op_morph = *)
-(* match opp with *)
-(* | Some opp -> *)
-(* (let opp_m = *)
-(* try default_morphism ~filter:is_endomorphism opp *)
-(* with Not_found -> *)
-(* error "ring opposite should be declared as a morphism" in *)
-(* let op_morph = *)
-(* op_morph r add mul opp req add_m.lem mul_m.lem opp_m.lem in *)
-(* msgnl *)
-(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\""++spc()++ *)
-(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *)
-(* str"\","++spc()++ str"\""++pr_constr mul_m.morphism_theory++ *)
-(* str"\""++spc()++str"and \""++pr_constr opp_m.morphism_theory++ *)
-(* str"\""); *)
-(* op_morph) *)
-(* | None -> *)
-(* (msgnl *)
-(* (str"Using setoid \""++pr_constr rel.rel_aeq++str"\"" ++ spc() ++ *)
-(* str"and morphisms \""++pr_constr add_m.morphism_theory++ *)
-(* str"\""++spc()++str"and \""++ *)
-(* pr_constr mul_m.morphism_theory++str"\""); *)
-(* op_smorph r add mul req add_m.lem mul_m.lem) in *)
-(* (setoid,op_morph) *)
-
let ring_equality env evd (r,add,mul,opp,req) =
match EConstr.kind !evd req with
| App (f, [| _ |]) when eq_constr_nounivs !evd f (Lazy.force coq_eq) ->
@@ -657,7 +601,8 @@ let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div
let _ =
Lib.add_leaf name
(theory_to_obj
- { ring_carrier = r;
+ { ring_name = name;
+ ring_carrier = r;
ring_req = req;
ring_setoid = sth;
ring_ext = params.(1);
@@ -835,19 +780,18 @@ let dest_field env evd th_spec =
| _ -> error "bad field structure"
let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table"
-let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table"
let print_fields () =
Feedback.msg_notice (strbrk "The following field structures have been declared:");
- Spmap.iter (fun fn fi ->
+ Cmap.iter (fun _carrier fi ->
let env = Global.env () in
let sigma = Evd.from_env env in
Feedback.msg_notice
(hov 2
- (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+ (Id.print fi.field_name ++ spc() ++
str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
- ) !field_from_name
+ ) !field_from_carrier
let field_for_carrier r = Cmap.find r !field_from_carrier
@@ -871,8 +815,7 @@ let find_field_structure env sigma l =
| [] -> assert false
let add_field_entry (sp,_kn) e =
- field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier;
- field_from_name := Spmap.add sp e !field_from_name
+ field_from_carrier := Cmap.add e.field_carrier e !field_from_carrier
let subst_th (subst,th) =
let c' = subst_mps subst th.field_carrier in
@@ -898,7 +841,8 @@ let subst_th (subst,th) =
pretac' == th.field_pre_tac &&
posttac' == th.field_post_tac then th
else
- { field_carrier = c';
+ { field_name = th.field_name;
+ field_carrier = c';
field_req = eq';
field_cst_tac = tac';
field_pow_tac = pow_tac';
@@ -983,7 +927,8 @@ let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign od
let _ =
Lib.add_leaf name
(ftheory_to_obj
- { field_carrier = r;
+ { field_name = name;
+ field_carrier = r;
field_req = req;
field_cst_tac = cst_tac;
field_pow_tac = pow_tac;
diff --git a/plugins/setoid_ring/newring_ast.ml b/plugins/setoid_ring/newring_ast.ml
index 0a3e7bd9ca..b81f5f7d14 100644
--- a/plugins/setoid_ring/newring_ast.ml
+++ b/plugins/setoid_ring/newring_ast.ml
@@ -40,7 +40,8 @@ type 'constr field_mod =
| Inject of constr_expr
type ring_info =
- { ring_carrier : types;
+ { ring_name : Names.Id.t;
+ ring_carrier : types;
ring_req : constr;
ring_setoid : constr;
ring_ext : constr;
@@ -54,7 +55,8 @@ type ring_info =
ring_post_tac : glob_tactic_expr }
type field_info =
- { field_carrier : types;
+ { field_name : Names.Id.t;
+ field_carrier : types;
field_req : constr;
field_cst_tac : glob_tactic_expr;
field_pow_tac : glob_tactic_expr;
diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli
index 0a3e7bd9ca..b81f5f7d14 100644
--- a/plugins/setoid_ring/newring_ast.mli
+++ b/plugins/setoid_ring/newring_ast.mli
@@ -40,7 +40,8 @@ type 'constr field_mod =
| Inject of constr_expr
type ring_info =
- { ring_carrier : types;
+ { ring_name : Names.Id.t;
+ ring_carrier : types;
ring_req : constr;
ring_setoid : constr;
ring_ext : constr;
@@ -54,7 +55,8 @@ type ring_info =
ring_post_tac : glob_tactic_expr }
type field_info =
- { field_carrier : types;
+ { field_name : Names.Id.t;
+ field_carrier : types;
field_req : constr;
field_cst_tac : glob_tactic_expr;
field_pow_tac : glob_tactic_expr;
diff --git a/stm/stm.ml b/stm/stm.ml
index 7f0632bd7c..1042061021 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -2617,13 +2617,10 @@ let dirpath_of_file f =
let new_doc { doc_type ; iload_path; require_libs; stm_options } =
- let load_objs libs =
- let rq_file (dir, from, exp) =
- let mp = Libnames.qualid_of_string dir in
- let mfrom = Option.map Libnames.qualid_of_string from in
- Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
- List.(iter rq_file (rev libs))
- in
+ let require_file (dir, from, exp) =
+ let mp = Libnames.qualid_of_string dir in
+ let mfrom = Option.map Libnames.qualid_of_string from in
+ Flags.silently (Vernacentries.vernac_require mfrom exp) [mp] in
(* Set the options from the new documents *)
AsyncOpts.cur_opt := stm_options;
@@ -2662,7 +2659,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } =
end;
(* Import initial libraries. *)
- load_objs require_libs;
+ List.iter require_file require_libs;
(* We record the state at this point! *)
State.define ~doc ~cache:true ~redefine:true (fun () -> ()) Stateid.initial;
diff --git a/test-suite/output/NoAxiomFromR.out b/test-suite/output/NoAxiomFromR.out
new file mode 100644
index 0000000000..7d7c521343
--- /dev/null
+++ b/test-suite/output/NoAxiomFromR.out
@@ -0,0 +1 @@
+Closed under the global context
diff --git a/test-suite/output/NoAxiomFromR.v b/test-suite/output/NoAxiomFromR.v
new file mode 100644
index 0000000000..9cf6879699
--- /dev/null
+++ b/test-suite/output/NoAxiomFromR.v
@@ -0,0 +1,10 @@
+Require Import Psatz.
+
+Inductive TT : Set :=
+| C : nat -> TT.
+
+Lemma lem4 : forall (n m : nat),
+S m <= m -> C (S m) <> C n -> False.
+Proof. firstorder. Qed.
+
+Print Assumptions lem4.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 3e0bf1d8ae..6984a7c2b6 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -243,6 +243,19 @@ Proof.
rewrite Hfst; rewrite Hsnd; reflexivity.
Qed.
+Lemma pair_equal_spec :
+ forall (A B : Type) (a1 a2 : A) (b1 b2 : B),
+ (a1, b1) = (a2, b2) <-> a1 = a2 /\ b1 = b2.
+Proof with auto.
+ split; intros.
+ - split.
+ + replace a1 with (fst (a1, b1)); replace a2 with (fst (a2, b2))...
+ rewrite H...
+ + replace b1 with (snd (a1, b1)); replace b2 with (snd (a2, b2))...
+ rewrite H...
+ - destruct H; subst...
+Qed.
+
Definition prod_uncurry (A B C:Type) (f:A * B -> C)
(x:A) (y:B) : C := f (x,y).
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index f45317ba50..38723e291f 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -536,6 +536,26 @@ Section Elts.
simpl in *. apply IHn. auto with arith.
Qed.
+ (** Results directly relating [nth] and [nth_error] *)
+
+ Lemma nth_error_nth : forall (l : list A) (n : nat) (x d : A),
+ nth_error l n = Some x -> nth n l d = x.
+ Proof.
+ intros l n x d H.
+ apply nth_error_split in H. destruct H as [l1 [l2 [H H']]].
+ subst. rewrite app_nth2; [|auto].
+ rewrite Nat.sub_diag. reflexivity.
+ Qed.
+
+ Lemma nth_error_nth' : forall (l : list A) (n : nat) (d : A),
+ n < length l -> nth_error l n = Some (nth n l d).
+ Proof.
+ intros l n d H.
+ apply nth_split with (d:=d) in H. destruct H as [l1 [l2 [H H']]].
+ subst. rewrite H. rewrite nth_error_app2; [|auto].
+ rewrite app_nth2; [| auto]. repeat (rewrite Nat.sub_diag). reflexivity.
+ Qed.
+
(*****************)
(** ** Remove *)
(*****************)
@@ -1234,11 +1254,11 @@ End Fold_Right_Recursor.
destruct (f x); simpl; now rewrite IH.
Qed.
- Lemma concat_filter_map : forall (l : list (list A)) (f : A -> bool),
+ Lemma concat_filter_map : forall (l : list (list A)),
concat (map filter l) = filter (concat l).
Proof.
induction l as [| v l IHl]; [auto|].
- simpl. rewrite (IHl f). rewrite filter_app. reflexivity.
+ simpl. rewrite IHl. rewrite filter_app. reflexivity.
Qed.
(** [find] *)
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 75298855b2..3b108b485a 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1692,7 +1692,6 @@ Proof.
exact H.
now apply not_INR in H.
Qed.
-Hint Resolve INR_eq: real.
Lemma INR_le : forall n m:nat, INR n <= INR m -> (n <= m)%nat.
Proof.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 20a8581d46..cba4780bd4 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -189,6 +189,16 @@ Fixpoint append {A}{n}{p} (v:t A n) (w:t A p):t A (n+p) :=
Infix "++" := append.
+(** Split a vector into two parts *)
+Fixpoint splitat {A} (l : nat) {r : nat} :
+ t A (l + r) -> t A l * t A r :=
+ match l with
+ | 0 => fun v => ([], v)
+ | S l' => fun v =>
+ let (v1, v2) := splitat l' (tl v) in
+ (hd v::v1, v2)
+ end.
+
(** Two definitions of the tail recursive function that appends two lists but
reverses the first one *)
diff --git a/theories/Vectors/VectorSpec.v b/theories/Vectors/VectorSpec.v
index 55a55c0b2f..b27566458e 100644
--- a/theories/Vectors/VectorSpec.v
+++ b/theories/Vectors/VectorSpec.v
@@ -153,3 +153,37 @@ Proof.
- destruct v. inversion le. simpl. apply f_equal. apply IHp.
Qed.
+Lemma uncons_cons {A} : forall {n : nat} (a : A) (v : t A n),
+ uncons (a::v) = (a,v).
+Proof. reflexivity. Qed.
+
+Lemma append_comm_cons {A} : forall {n m : nat} (v : t A n) (w : t A m) (a : A),
+ a :: (v ++ w) = (a :: v) ++ w.
+Proof. reflexivity. Qed.
+
+Lemma splitat_append {A} : forall {n m : nat} (v : t A n) (w : t A m),
+ splitat n (v ++ w) = (v, w).
+Proof with simpl; auto.
+ intros n m v.
+ generalize dependent m.
+ induction v; intros...
+ rewrite IHv...
+Qed.
+
+Lemma append_splitat {A} : forall {n m : nat} (v : t A n) (w : t A m) (vw : t A (n+m)),
+ splitat n vw = (v, w) ->
+ vw = v ++ w.
+Proof with auto.
+ intros n m v.
+ generalize dependent m.
+ induction v; intros; inversion H...
+ destruct (splitat n (tl vw)) as [v' w'] eqn:Heq.
+ apply pair_equal_spec in H1.
+ destruct H1; subst.
+ rewrite <- append_comm_cons.
+ rewrite (eta vw).
+ apply cons_inj in H0.
+ destruct H0; subst.
+ f_equal...
+ apply IHv...
+Qed.
diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml
index fe5361c156..3600658e23 100644
--- a/toplevel/ccompile.ml
+++ b/toplevel/ccompile.ml
@@ -39,7 +39,7 @@ let load_vernacular opts ~state =
if !Flags.beautify
then Flags.with_option Flags.beautify_file load_vernac f_in
else load_vernac s
- ) state (List.rev opts.pre.load_vernacular_list)
+ ) state opts.pre.load_vernacular_list
let load_init_vernaculars opts ~state =
let state = load_init_file opts ~state in
@@ -193,7 +193,7 @@ let compile_file opts copts (f_in, echo) =
compile opts copts ~echo ~f_in ~f_out
let compile_files opts copts =
- let compile_list = List.rev copts.compile_list in
+ let compile_list = copts.compile_list in
List.iter (compile_file opts copts) compile_list
(******************************************************************************)
@@ -205,7 +205,7 @@ let check_vio_tasks copts =
let f_in = ensure ".vio" f f in
ensure_exists f_in;
Vio_checking.check_vio (n,f_in) && acc)
- true (List.rev copts.vio_tasks) in
+ true copts.vio_tasks in
if not rc then fatal_error Pp.(str "VIO Task Check failed")
(* vio files *)
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 0490c35970..113b1fb5d7 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -547,6 +547,23 @@ let parse_args ~help ~init arglist : t * string list =
parse init
with any -> fatal_error any
+(* We need to reverse a few lists *)
+let parse_args ~help ~init args =
+ let opts, extra = parse_args ~help ~init args in
+ let opts =
+ { opts with
+ pre = { opts.pre with
+ ml_includes = List.rev opts.pre.ml_includes
+ ; vo_includes = List.rev opts.pre.vo_includes
+ ; vo_requires = List.rev opts.pre.vo_requires
+ ; load_vernacular_list = List.rev opts.pre.load_vernacular_list
+ }
+ ; config = { opts.config with
+ set_options = List.rev opts.config.set_options
+ } ;
+ } in
+ opts, extra
+
(******************************************************************************)
(* Startup LoadPath and Modules *)
(******************************************************************************)
@@ -557,7 +574,7 @@ let require_libs opts =
if opts.pre.load_init then prelude_data :: opts.pre.vo_requires else opts.pre.vo_requires
let cmdline_load_path opts =
- List.rev opts.pre.vo_includes @ List.(rev opts.pre.ml_includes)
+ opts.pre.ml_includes @ opts.pre.vo_includes
let build_load_path opts =
Coqinit.libs_init_load_path ~load_init:opts.pre.load_init @
diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml
index 0b5481fe72..c4e3571281 100644
--- a/toplevel/coqcargs.ml
+++ b/toplevel/coqcargs.ml
@@ -210,3 +210,11 @@ let parse arglist : t =
check_compilation_output_name_consistency args;
args
with any -> fatal_error any
+
+let parse args =
+ let opts = parse args in
+ { opts with
+ compile_list = List.rev opts.compile_list
+ ; vio_tasks = List.rev opts.vio_tasks
+ ; vio_files = List.rev opts.vio_files
+ }
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index e9d8263b85..bca6b48499 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -169,6 +169,6 @@ let beautify_pass ~doc ~comments ~ids ~filename =
let load_vernac ~echo ~check ~interactive ~state filename =
let ostate, ids, comments = load_vernac_core ~echo ~check ~interactive ~state filename in
(* Pass for beautify *)
- if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:List.(rev ids) ~filename;
+ if !Flags.beautify then beautify_pass ~doc:ostate.State.doc ~comments ~ids:(List.rev ids) ~filename;
(* End pass *)
ostate
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 06:53:31 +0000