diff options
33 files changed, 168 insertions, 65 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 006565df5c..6d1e6d788a 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -138,8 +138,8 @@ make() if [ -z "${MAKEFLAGS+x}" ] && [ -n "${NJOBS}" ]; then # Not submake and parallel make requested - command make --output-sync -j "$NJOBS" "$@" + command make -j "$NJOBS" "$@" else - command make --output-sync "$@" + command make "$@" fi } diff --git a/dev/ci/ci-paramcoq.sh b/dev/ci/ci-paramcoq.sh index 1b2d6a73a2..d2e0ee89bf 100755 --- a/dev/ci/ci-paramcoq.sh +++ b/dev/ci/ci-paramcoq.sh @@ -5,7 +5,4 @@ ci_dir="$(dirname "$0")" git_download paramcoq -# Typically flaky on our worker configuration -# https://gitlab.com/coq/coq/-/jobs/1144081161 -export COQEXTRAFLAGS='-native-compiler no' ( cd "${CI_BUILD_DIR}/paramcoq" && make && make install && cd test-suite && make examples) diff --git a/dev/shim/dune b/dev/shim/dune index e4cc7699f0..2c7f9c3fa9 100644 --- a/dev/shim/dune +++ b/dev/shim/dune @@ -26,7 +26,7 @@ (targets coqbyte-prelude) (deps %{bin:coqtop.byte} - %{lib:coq-core.kernel:../../stublibs/dllbyterun_stubs.so} + %{lib:coq-core.kernel:../../stublibs/dllcoqrun_stubs.so} %{project_root}/theories/Init/Prelude.vo) (action (with-stdout-to %{targets} diff --git a/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst b/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst new file mode 100644 index 0000000000..7831d10392 --- /dev/null +++ b/doc/changelog/07-vernac-commands-and-options/14093-fix-14092.rst @@ -0,0 +1,6 @@ +- **Added:** + The Ltac2 grammar can now be printed using the + Print Grammar ltac2 command + (`#14093 <https://github.com/coq/coq/pull/14093>`_, + fixes `#14092 <https://github.com/coq/coq/issues/14092>`_, + by Pierre-Marie Pédrot). diff --git a/doc/changelog/10-standard-library/14008-Cantor-pairing.rst b/doc/changelog/10-standard-library/14008-Cantor-pairing.rst new file mode 100644 index 0000000000..4c217f3fb0 --- /dev/null +++ b/doc/changelog/10-standard-library/14008-Cantor-pairing.rst @@ -0,0 +1,6 @@ +- **Added:** + ``Cantor.v`` containing the Cantor pairing function and its inverse. + ``Cantor.to_nat : nat * nat -> nat`` and ``Cantor.of_nat : nat -> nat * nat`` + are the respective bijections between ``nat * nat`` and ``nat``. + (`#14008 <https://github.com/coq/coq/pull/14008>`_, + by Andrej Dudenhefner). @@ -63,3 +63,6 @@ (files (refman-html as html/refman) (refman-pdf as pdf/refman)) (section doc) (package coq-doc)) + +(documentation + (package coq-doc)) diff --git a/doc/index.mld b/doc/index.mld new file mode 100644 index 0000000000..3a1979bc62 --- /dev/null +++ b/doc/index.mld @@ -0,0 +1,3 @@ +{0 coq-doc } + +The coq-doc package only contains user documentation on the Coq proof assistant and no OCaml library. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 453e878a5d..d212256765 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -467,6 +467,7 @@ Displaying information about notations - `tactic` - for currently-defined tactic notations, :token:`tactic`\s and tacticals (corresponding to :token:`ltac_expr` in the documentation). - `vernac` - for :token:`command`\s + - `ltac2` - for Ltac2 notations (corresponding to :token:`ltac2_expr`) This command doesn't display all nonterminals of the grammar. For example, productions shown by `Print Grammar tactic` refer to nonterminals `tactic_then_locality` diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index d67906c4a8..6fda3b06ce 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -135,6 +135,7 @@ through the <tt>Require Import</tt> command.</p> theories/Arith/Bool_nat.v theories/Arith/Factorial.v theories/Arith/Wf_nat.v + theories/Arith/Cantor.v </dd> <dt> <b>PArith</b>: @@ -35,3 +35,6 @@ (deps test-suite/summary.log)) ; (dirs (:standard _build_ci)) + +(documentation + (package coq)) diff --git a/engine/univProblem.ml b/engine/univProblem.ml index 7ac6ca1180..10ee601f3f 100644 --- a/engine/univProblem.ml +++ b/engine/univProblem.ml @@ -9,7 +9,6 @@ (************************************************************************) open Univ -open UnivSubst type t = | ULe of Universe.t * Universe.t @@ -22,24 +21,6 @@ let is_trivial = function | ULe (u, v) | UEq (u, v) -> Universe.equal u v | ULub (u, v) | UWeak (u, v) -> Level.equal u v -let subst_univs fn = function - | ULe (u, v) -> - let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in - if Universe.equal u' v' then None - else Some (ULe (u',v')) - | UEq (u, v) -> - let u' = subst_univs_universe fn u and v' = subst_univs_universe fn v in - if Universe.equal u' v' then None - else Some (UEq (u',v')) - | ULub (u, v) -> - let u' = level_subst_of fn u and v' = level_subst_of fn v in - if Level.equal u' v' then None - else Some (ULub (u',v')) - | UWeak (u, v) -> - let u' = level_subst_of fn u and v' = level_subst_of fn v in - if Level.equal u' v' then None - else Some (UWeak (u',v')) - module Set = struct module S = Set.Make( struct @@ -88,11 +69,6 @@ module Set = struct let equal x y = x == y || equal x y - - let subst_univs subst csts = - fold - (fun c -> Option.fold_right add (subst_univs subst c)) - csts empty end type 'a accumulator = Set.t -> 'a -> 'a option diff --git a/engine/univProblem.mli b/engine/univProblem.mli index 575f5ac847..6c7a11f529 100644 --- a/engine/univProblem.mli +++ b/engine/univProblem.mli @@ -32,8 +32,6 @@ module Set : sig include Set.S with type elt = t val pr : t -> Pp.t - - val subst_univs : universe_subst_fn -> t -> t end type 'a accumulator = Set.t -> 'a -> 'a option diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index 20e9f0134f..dc616066c2 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -538,7 +538,7 @@ struct let implicit = BoolOpt ["Printing"; "Implicit"] let coercions = BoolOpt ["Printing"; "Coercions"] - let raw_matching = BoolOpt ["Printing"; "Matching"] + let nested_matching = BoolOpt ["Printing"; "Matching"] let notations = BoolOpt ["Printing"; "Notations"] let parentheses = BoolOpt ["Printing"; "Parentheses"] let all_basic = BoolOpt ["Printing"; "All"] @@ -553,8 +553,8 @@ struct let bool_items = [ { opts = [implicit]; init = false; label = "Display _implicit arguments" }; { opts = [coercions]; init = false; label = "Display _coercions" }; - { opts = [raw_matching]; init = true; - label = "Display raw _matching expressions" }; + { opts = [nested_matching]; init = true; + label = "Display nested _matching expressions" }; { opts = [notations]; init = true; label = "Display _notations" }; { opts = [parentheses]; init = false; label = "Display _parentheses" }; { opts = [all_basic]; init = false; diff --git a/ide/coqide/coq_commands.ml b/ide/coqide/coq_commands.ml index 6e02d7fed1..3a080d5f51 100644 --- a/ide/coqide/coq_commands.ml +++ b/ide/coqide/coq_commands.ml @@ -93,7 +93,6 @@ let commands = [ ]; ["Read Module"; "Record"; - "Variant"; "Remark"; "Remove LoadPath"; "Remove Printing Constructor"; diff --git a/ide/coqide/coqide_ui.ml b/ide/coqide/coqide_ui.ml index badfabf07e..82eca905ea 100644 --- a/ide/coqide/coqide_ui.ml +++ b/ide/coqide/coqide_ui.ml @@ -77,7 +77,7 @@ let init () = \n <separator/>\ \n <menuitem action='Display implicit arguments' />\ \n <menuitem action='Display coercions' />\ -\n <menuitem action='Display raw matching expressions' />\ +\n <menuitem action='Display nested matching expressions' />\ \n <menuitem action='Display notations' />\ \n <menuitem action='Display parentheses' />\ \n <menuitem action='Display all basic low-level contents' />\ diff --git a/ide/coqide/dune b/ide/coqide/dune index 4bb4672cd4..d2642f77bf 100644 --- a/ide/coqide/dune +++ b/ide/coqide/dune @@ -51,6 +51,9 @@ (modes exe byte) (libraries coqide_gui)) +(documentation + (package coqide)) + ; Input-method bindings (executable (name default_bindings_src) diff --git a/ide/coqide/index.mld b/ide/coqide/index.mld new file mode 100644 index 0000000000..8852a2a7eb --- /dev/null +++ b/ide/coqide/index.mld @@ -0,0 +1,3 @@ +{0 coqide } + +The coqide package only contains the CoqIDE executable and no OCaml library. diff --git a/index.mld b/index.mld new file mode 100644 index 0000000000..706688656e --- /dev/null +++ b/index.mld @@ -0,0 +1,5 @@ +{0 coq } + +The coq package is a virtual package gathering the coq-core and coq-stdlib packages. + +For the documentation of the OCaml API of Coq, see the {{: ../coq-core/index.html } coq-core } package. diff --git a/lib/pp.mli b/lib/pp.mli index b3c2301d34..865f97166f 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -171,7 +171,7 @@ val prvecti_with_sep : val pr_enum : ('a -> t) -> 'a list -> t (** [pr_enum pr [a ; b ; ... ; c]] outputs - [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c]. *) + [pr a ++ str "," ++ spc () ++ pr b ++ str "," ++ spc () ++ ... ++ str "and" ++ spc () ++ pr c]. *) val pr_sequence : ('a -> t) -> 'a list -> t (** Sequence of objects separated by space (unless an element is empty). *) @@ -188,7 +188,6 @@ val pp_with : Format.formatter -> t -> unit val string_of_ppcmds : t -> string - (** Tag prefix to start a multi-token diff span *) val start_pfx : string diff --git a/library/lib.ml b/library/lib.ml index fa0a95d366..3172511c26 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -280,7 +280,7 @@ let start_mod is_type export id mp fs = else Nametab.exists_dir dir in if exists then - user_err ~hdr:"open_module" (Id.print id ++ str " already exists"); + user_err ~hdr:"open_module" (Id.print id ++ str " already exists."); add_entry (make_foname id) (OpenedModule (is_type,export,prefix,fs)); lib_state := { !lib_state with path_prefix = prefix} ; prefix diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 44d3b44077..b529bba3f5 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -298,7 +298,7 @@ let meta_reducible_instance env evd b = if not is_coerce then irec g else u with Not_found -> u) | Proj (p,c) when isMeta evd c || isCast evd c && isMeta evd (pi1 (destCast evd c)) (* What if two nested casts? *) -> - let m = try destMeta evd c with _ -> destMeta evd (pi1 (destCast evd c)) (* idem *) in + let m = try destMeta evd c with DestKO -> destMeta evd (pi1 (destCast evd c)) (* idem *) in (match try let g, s = Metamap.find m metas in diff --git a/theories/Arith/Cantor.v b/theories/Arith/Cantor.v new file mode 100644 index 0000000000..b63d970db7 --- /dev/null +++ b/theories/Arith/Cantor.v @@ -0,0 +1,88 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** Implementation of the Cantor pairing and its inverse function *) + +Require Import PeanoNat Lia. + +(** Bijections between [nat * nat] and [nat] *) + +(** Cantor pairing [to_nat] *) + +Definition to_nat '(x, y) : nat := + y + (nat_rec _ 0 (fun i m => (S i) + m) (y + x)). + +(** Cantor pairing inverse [of_nat] *) + +Definition of_nat (n : nat) : nat * nat := + nat_rec _ (0, 0) (fun _ '(x, y) => + match x with | S x => (x, S y) | _ => (S y, 0) end) n. + +(** [of_nat] is the left inverse for [to_nat] *) + +Lemma cancel_of_to p : of_nat (to_nat p) = p. +Proof. + enough (H : forall n p, to_nat p = n -> of_nat n = p) by now apply H. + intro n. induction n as [|n IHn]. + - now intros [[|?] [|?]]. + - intros [x [|y]]. + + destruct x as [|x]; [discriminate|]. + intros [=H]. cbn. fold (of_nat n). + rewrite (IHn (0, x)); [reflexivity|]. + rewrite <- H. cbn. now rewrite PeanoNat.Nat.add_0_r. + + intros [=H]. cbn. fold (of_nat n). + rewrite (IHn (S x, y)); [reflexivity|]. + rewrite <- H. cbn. now rewrite Nat.add_succ_r. +Qed. + +(** [to_nat] is injective *) + +Corollary to_nat_inj p q : to_nat p = to_nat q -> p = q. +Proof. + intros H %(f_equal of_nat). now rewrite ?cancel_of_to in H. +Qed. + +(** [to_nat] is the left inverse for [of_nat] *) + +Lemma cancel_to_of n : to_nat (of_nat n) = n. +Proof. + induction n as [|n IHn]; [reflexivity|]. + cbn. fold (of_nat n). destruct (of_nat n) as [[|x] y]. + - rewrite <- IHn. cbn. now rewrite PeanoNat.Nat.add_0_r. + - rewrite <- IHn. cbn. now rewrite (Nat.add_succ_r y x). +Qed. + +(** [of_nat] is injective *) + +Corollary of_nat_inj n m : of_nat n = of_nat m -> n = m. +Proof. + intros H %(f_equal to_nat). now rewrite ?cancel_to_of in H. +Qed. + +(** Polynomial specifications of [to_nat] *) + +Lemma to_nat_spec x y : + to_nat (x, y) * 2 = y * 2 + (y + x) * S (y + x). +Proof. + cbn. induction (y + x) as [|n IHn]; cbn; lia. +Qed. + +Lemma to_nat_spec2 x y : + to_nat (x, y) = y + (y + x) * S (y + x) / 2. +Proof. + now rewrite <- Nat.div_add_l, <- to_nat_spec, Nat.div_mul. +Qed. + +(** [to_nat] is non-decreasing in (the sum of) pair components *) + +Lemma to_nat_non_decreasing x y : y + x <= to_nat (x, y). +Proof. + pose proof (to_nat_spec x y). nia. +Qed. diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 3dac62c476..23bc396fd7 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -676,7 +676,7 @@ Qed. We show instead that functional relation reification and the functional form of the axiom of choice are equivalent on decidable - relation with [nat] as codomain + relations with [nat] as codomain. *) Require Import Wf_nat. diff --git a/theories/Logic/ExtensionalityFacts.v b/theories/Logic/ExtensionalityFacts.v index 4735d6c9ca..a151cca3af 100644 --- a/theories/Logic/ExtensionalityFacts.v +++ b/theories/Logic/ExtensionalityFacts.v @@ -43,7 +43,7 @@ Definition is_inverse A B f g := (forall a:A, g (f a) = a) /\ (forall b:B, f (g #[universes(template)] Record Delta A := { pi1:A; pi2:A; eq:pi1=pi2 }. -Definition delta {A} (a:A) := {|pi1 := a; pi2 := a; eq := eq_refl a |}. +Definition delta {A} (a:A) := {| pi1 := a; pi2 := a; eq := eq_refl a |}. Arguments pi1 {A} _. Arguments pi2 {A} _. diff --git a/theories/dune b/theories/dune index ced818c3ba..57b97f080c 100644 --- a/theories/dune +++ b/theories/dune @@ -33,3 +33,6 @@ coq-core.plugins.derive)) (include_subdirs qualified) + +(documentation + (package coq-stdlib)) diff --git a/theories/index.mld b/theories/index.mld new file mode 100644 index 0000000000..360864342b --- /dev/null +++ b/theories/index.mld @@ -0,0 +1,3 @@ +{0 coq-stdlib } + +The coq-stdlib package only contains Coq theory files for the standard library and no OCaml libraries. diff --git a/theories/micromega/OrderedRing.v b/theories/micromega/OrderedRing.v index 5fa3740ab1..bfbd6fd8d3 100644 --- a/theories/micromega/OrderedRing.v +++ b/theories/micromega/OrderedRing.v @@ -423,7 +423,7 @@ Qed. (* The following theorems are used to build a morphism from Z to R and prove its properties in ZCoeff.v. They are not used in RingMicromega.v. *) -(* Surprisingly, multilication is needed to prove the following theorem *) +(* Surprisingly, multiplication is needed to prove the following theorem *) Theorem Ropp_neg_pos : forall n : R, - n < 0 <-> 0 < n. Proof. @@ -457,4 +457,3 @@ apply Rtimes_pos_pos. assumption. now apply -> Rlt_lt_minus. Qed.*) End STRICT_ORDERED_RING. - diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v index 9881e73f76..dd31b998d4 100644 --- a/theories/micromega/ZifyInst.v +++ b/theories/micromega/ZifyInst.v @@ -307,15 +307,15 @@ Instance Op_N_mul : BinOp N.mul := Add Zify BinOp Op_N_mul. Instance Op_N_sub : BinOp N.sub := - {| TBOp := fun x y => Z.max 0 (x - y) ; TBOpInj := N2Z.inj_sub_max|}. + {| TBOp := fun x y => Z.max 0 (x - y) ; TBOpInj := N2Z.inj_sub_max |}. Add Zify BinOp Op_N_sub. Instance Op_N_div : BinOp N.div := - {| TBOp := Z.div ; TBOpInj := N2Z.inj_div|}. + {| TBOp := Z.div ; TBOpInj := N2Z.inj_div |}. Add Zify BinOp Op_N_div. Instance Op_N_mod : BinOp N.modulo := - {| TBOp := Z.rem ; TBOpInj := N2Z.inj_rem|}. + {| TBOp := Z.rem ; TBOpInj := N2Z.inj_rem |}. Add Zify BinOp Op_N_mod. Instance Op_N_pred : UnOp N.pred := @@ -332,19 +332,19 @@ Add Zify UnOp Op_N_succ. (* zify_Z_rel *) Instance Op_Z_ge : BinRel Z.ge := - {| TR := Z.ge ; TRInj := fun x y => iff_refl (x>= y)|}. + {| TR := Z.ge ; TRInj := fun x y => iff_refl (x>= y) |}. Add Zify BinRel Op_Z_ge. Instance Op_Z_lt : BinRel Z.lt := - {| TR := Z.lt ; TRInj := fun x y => iff_refl (x < y)|}. + {| TR := Z.lt ; TRInj := fun x y => iff_refl (x < y) |}. Add Zify BinRel Op_Z_lt. Instance Op_Z_gt : BinRel Z.gt := - {| TR := Z.gt ;TRInj := fun x y => iff_refl (x > y)|}. + {| TR := Z.gt ;TRInj := fun x y => iff_refl (x > y) |}. Add Zify BinRel Op_Z_gt. Instance Op_Z_le : BinRel Z.le := - {| TR := Z.le ;TRInj := fun x y => iff_refl (x <= y)|}. + {| TR := Z.le ;TRInj := fun x y => iff_refl (x <= y) |}. Add Zify BinRel Op_Z_le. Instance Op_eqZ : BinRel (@eq Z) := @@ -460,7 +460,7 @@ Add Zify UnOp Op_Z_to_nat. (** Specification of derived operators over Z *) Instance ZmaxSpec : BinOpSpec Z.max := - {| BPred := fun n m r => n < m /\ r = m \/ m <= n /\ r = n ; BSpec := Z.max_spec|}. + {| BPred := fun n m r => n < m /\ r = m \/ m <= n /\ r = n ; BSpec := Z.max_spec |}. Add Zify BinOpSpec ZmaxSpec. Instance ZminSpec : BinOpSpec Z.min := @@ -470,12 +470,12 @@ Add Zify BinOpSpec ZminSpec. Instance ZsgnSpec : UnOpSpec Z.sgn := {| UPred := fun n r : Z => 0 < n /\ r = 1 \/ 0 = n /\ r = 0 \/ n < 0 /\ r = - (1) ; - USpec := Z.sgn_spec|}. + USpec := Z.sgn_spec |}. Add Zify UnOpSpec ZsgnSpec. Instance ZabsSpec : UnOpSpec Z.abs := {| UPred := fun n r: Z => 0 <= n /\ r = n \/ n < 0 /\ r = - n ; - USpec := Z.abs_spec|}. + USpec := Z.abs_spec |}. Add Zify UnOpSpec ZabsSpec. (** Saturate positivity constraints *) diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml index 6be5ba80d5..7af530ab0f 100644 --- a/user-contrib/Ltac2/tac2entries.ml +++ b/user-contrib/Ltac2/tac2entries.ml @@ -50,6 +50,12 @@ let q_pose = Pcoq.Entry.create "q_pose" let q_assert = Pcoq.Entry.create "q_assert" end +let () = + let entries = [ + Pcoq.AnyEntry Pltac.ltac2_expr; + ] in + Pcoq.register_grammars_by_name "ltac2" entries + (** Tactic definition *) type tacdef = { diff --git a/user-contrib/Ltac2/tac2intern.ml b/user-contrib/Ltac2/tac2intern.ml index 90c8528203..206f4df19d 100644 --- a/user-contrib/Ltac2/tac2intern.ml +++ b/user-contrib/Ltac2/tac2intern.ml @@ -467,7 +467,9 @@ let polymorphic ((n, t) : type_scheme) : mix_type_scheme = let warn_not_unit = CWarnings.create ~name:"not-unit" ~category:"ltac" - (fun () -> strbrk "The following expression should have type unit.") + (fun (env, t) -> + strbrk "The following expression should have type unit but has type " ++ + pr_glbtype env t ++ str ".") let warn_redundant_clause = CWarnings.create ~name:"redundant-clause" ~category:"ltac" @@ -480,7 +482,7 @@ let check_elt_unit loc env t = | GTypRef (Tuple 0, []) -> true | GTypRef _ -> false in - if not maybe_unit then warn_not_unit ?loc () + if not maybe_unit then warn_not_unit ?loc (env, t) let check_elt_empty loc env t = match kind env t with | GTypVar _ -> @@ -504,7 +506,7 @@ let check_unit ?loc t = | GTypRef (Tuple 0, []) -> true | GTypRef _ -> false in - if not maybe_unit then warn_not_unit ?loc () + if not maybe_unit then warn_not_unit ?loc (env, t) let check_redundant_clause = function | [] -> () diff --git a/vernac/declaremods.ml b/vernac/declaremods.ml index 15e6d4ef37..95e05556b9 100644 --- a/vernac/declaremods.ml +++ b/vernac/declaremods.ml @@ -216,7 +216,7 @@ let consistency_checks exists dir dirinfo = else if Nametab.exists_dir dir then user_err ~hdr:"consistency_checks" - (DirPath.print dir ++ str " already exists") + (DirPath.print dir ++ str " already exists.") let compute_visibility exists i = if exists then Nametab.Exactly i else Nametab.Until i diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 2fe402ff08..f9f65a8c30 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1664,7 +1664,7 @@ let add_notation_interpretation env decl_ntn = decl_ntn_scope = sc; } = decl_ntn in match interp_non_syntax_modifiers modifiers with - | None -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here") + | None -> CErrors.user_err (str"Only modifiers not affecting parsing are supported here.") | Some (only_parsing,only_printing,entry) -> let df' = add_notation_interpretation_core ~local:false df env entry c sc only_parsing false None in Dumpglob.dump_notation (loc,df') sc true @@ -1845,6 +1845,6 @@ let inCustomEntry : locality_flag * string -> obj = let declare_custom_entry local s = if Egramcoq.exists_custom_entry s then - user_err Pp.(str "Custom entry " ++ str s ++ str " already exists") + user_err Pp.(str "Custom entry " ++ str s ++ str " already exists.") else Lib.add_anonymous_leaf (inCustomEntry (local,s)) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e8d84a67a3..af40292f18 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1934,10 +1934,9 @@ let vernac_search ~pstate ~atts s gopt r = let open ComSearch in let gopt = query_command_selector gopt in let sigma, env = - match gopt with | None -> - (* 1st goal by default if it exists, otherwise no goal at all *) - (try get_goal_or_global_context ~pstate 1 - with _ -> let env = Global.env () in (Evd.from_env env, env)) + match gopt with + (* 1st goal by default if it exists, otherwise no goal at all *) + | None -> get_goal_or_global_context ~pstate 1 (* if goal selector is given and wrong, then let exceptions be raised. *) | Some g -> get_goal_or_global_context ~pstate g in interp_search env sigma s r |