diff options
98 files changed, 643 insertions, 246 deletions
diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS index 65c971ce76..d9136ee24b 100644 --- a/.github/CODEOWNERS +++ b/.github/CODEOWNERS @@ -6,11 +6,23 @@ /.github/ @maximedenes # Secondary maintainer @Zimmi48 +########## Build system ########## + +/Makefile* @gares + +/configure* @ejgallego + +/META.coq.in @ejgallego + +/dev/build/windows @MSoegtropIMC +# Secondary maintainer @maximedenes + ########## CI infrastructure ########## /dev/ci/ @coq/ci-maintainers /.travis.yml @coq/ci-maintainers /.gitlab-ci.yml @coq/ci-maintainers +/Makefile.ci @coq/ci-maintainers /dev/ci/user-overlays/*.sh @ghost # Trick to avoid getting review requests @@ -21,8 +33,7 @@ /dev/ci/*.bat @maximedenes # Secondary maintainer @SkySkimmer -/default.nix @Zimmi48 -# Secondary maintainer @vbgl +*.nix @coq/nix-maintainers ########## Documentation ########## @@ -43,6 +54,7 @@ # each time someone modifies the dev changelog /doc/ @coq/doc-maintainers +/Makefile.doc @coq/doc-maintainers /man/ @silene # Secondary maintainer @maximedenes @@ -258,6 +270,7 @@ ########## Dune ########## +/.ocamlinit @ejgallego /Makefile.dune @ejgallego /tools/coq_dune* @ejgallego /dune* @ejgallego @@ -301,25 +314,6 @@ /vernac/ @mattam82 # Secondary maintainer @maximedenes -########## Build system ########## - -/Makefile* @gares - -/configure* @ejgallego - -/META.coq.in @ejgallego - -/dev/build/windows @MSoegtropIMC -# Secondary maintainer @maximedenes - -# This file belongs to CI -/Makefile.ci @ejgallego -# Secondary maintainer @SkySkimmer - -# This file belongs to the doc -/Makefile.doc @maximedenes -# Secondary maintainer @silene - ########## Test suite ########## /test-suite/Makefile @gares diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 7f770feded..693a0b6bf0 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -89,6 +89,7 @@ after_script: - set +e .dune-template: &dune-template + dependencies: [] stage: build artifacts: name: "$CI_JOB_NAME" @@ -97,9 +98,7 @@ after_script: expire_in: 1 week script: - set -e - - echo 'start:coq.dune' - - make -f Makefile.dune world - - echo 'end:coq.dune' + - make -f Makefile.dune "$DUNE_TARGET" - set +e # every non build job must set dependencies otherwise all build @@ -217,10 +216,11 @@ build:edge+flambda: COQ_EXTRA_CONF: "-native-compiler yes -coqide opt -flambda-opts " COQ_EXTRA_CONF_QUOTE: "-O3 -unbox-closures" -build:egde:dune: +build:egde:dune:dev: <<: *dune-template variables: OPAM_SWITCH: edge + DUNE_TARGET: world windows64: <<: *windows-template @@ -234,6 +234,12 @@ windows32: except: - /^pr-.*$/ +pkg:dune-release: + <<: *dune-template + stage: test + variables: + OPAM_SWITCH: edge + DUNE_TARGET: release pkg:nix: image: nixorg/nix:latest # Minimal NixOS image which doesn't even contain git diff --git a/.ocamlinit b/.ocamlinit new file mode 100644 index 0000000000..3771334e12 --- /dev/null +++ b/.ocamlinit @@ -0,0 +1 @@ +#rectypes;; @@ -10,6 +10,11 @@ Notations - New support for autonomous grammars of terms, called "custom entries" (see chapter "Syntax extensions" of the reference manual). +- New command "Declare Scope" to explicitly declare a scope name + before any use of it. Implicit declaration of a scope at the time of + "Bind Scope", "Delimit Scope", "Undelimit Scope", or "Notation" is + deprecated. + Tactics - Added toplevel goal selector ! which expects a single focused goal. @@ -34,6 +39,10 @@ Tactics - Deprecated the Implicit Tactic family of commands. +- The default program obligation tactic uses a bounded proof search + instead of an unbounded and potentially non-terminating one now + (source of incompatibility). + - The `simple apply` tactic now respects the `Opaque` flag when called from Ltac (`auto` still does not respect it). @@ -48,6 +57,8 @@ Tactics may need to add `Require Import Lra` to your developments. For compatibility, we now define `fourier` as a deprecated alias of `lra`. +- The `romega` tactics have been deprecated; please use `lia` instead. + Focusing - Focusing bracket `{` now supports named goal selectors, @@ -177,6 +177,9 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; ########################################################################### camldevfiles: $(MERLINFILES) META.coq +# prevent submake dependency +META.coq.in $(MERLININFILES): ; + .merlin: .merlin.in cp -a "$<" "$@" diff --git a/Makefile.dune b/Makefile.dune index 6056151c0d..f90f555557 100644 --- a/Makefile.dune +++ b/Makefile.dune @@ -10,10 +10,11 @@ BUILD_CONTEXT=_build/default help: @echo "Welcome to Coq's Dune-based build system. Targets are:" - @echo " - states: build a minimal functional coqtop" - @echo " - world: build all binaries and libraries" - @echo " - clean: remove build directory and autogenerated files" - @echo " - help: show this message" + @echo " - states: build a minimal functional coqtop" + @echo " - world: build all binaries and libraries" + @echo " - release: build Coq in release mode" + @echo " - clean: remove build directory and autogenerated files" + @echo " - help: show this message" voboot: dune build $(DUNEOPT) @vodeps @@ -25,6 +26,9 @@ states: voboot world: voboot dune build $(DUNEOPT) @install +release: voboot + dune build $(DUNEOPT) -p coq + clean: dune clean diff --git a/coqpp/coqpp_ast.mli b/coqpp/coqpp_ast.mli index 39b4d2ab34..181c43615b 100644 --- a/coqpp/coqpp_ast.mli +++ b/coqpp/coqpp_ast.mli @@ -81,6 +81,7 @@ type grammar_ext = { type tactic_ext = { tacext_name : string; tacext_level : int option; + tacext_deprecated : code option; tacext_rules : tactic_rule list; } diff --git a/coqpp/coqpp_lex.mll b/coqpp/coqpp_lex.mll index 6c6562c204..bfa4e2b57b 100644 --- a/coqpp/coqpp_lex.mll +++ b/coqpp/coqpp_lex.mll @@ -95,6 +95,7 @@ rule extend = parse | "END" { END } | "DECLARE" { DECLARE } | "PLUGIN" { PLUGIN } +| "DEPRECATED" { DEPRECATED } (** Camlp5 specific keywords *) | "GLOBAL" { GLOBAL } | "FIRST" { FIRST } diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml index 1648167a27..a8ed95f5ba 100644 --- a/coqpp/coqpp_main.ml +++ b/coqpp/coqpp_main.ml @@ -316,10 +316,17 @@ let print_rules fmt rules = fprintf fmt "Tacentries.([@[<v>%a@]])" print_rules rules let print_ast fmt ext = + let deprecation fmt = + function + | None -> () + | Some { code } -> fprintf fmt "~deprecation:(%s) " code + in let pr fmt () = let level = match ext.tacext_level with None -> 0 | Some i -> i in - fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a" - plugin_name ext.tacext_name level print_rules ext.tacext_rules + fprintf fmt "Tacentries.tactic_extend %s \"%s\" ~level:%i %a%a" + plugin_name ext.tacext_name level + deprecation ext.tacext_deprecated + print_rules ext.tacext_rules in let () = fprintf fmt "let () = @[%a@]\n" pr () in () diff --git a/coqpp/coqpp_parse.mly b/coqpp/coqpp_parse.mly index baafd633c4..bf435fd247 100644 --- a/coqpp/coqpp_parse.mly +++ b/coqpp/coqpp_parse.mly @@ -62,7 +62,7 @@ let parse_user_entry s sep = %token <string> IDENT QUALID %token <string> STRING %token <int> INT -%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN +%token VERNAC TACTIC GRAMMAR EXTEND END DECLARE PLUGIN DEPRECATED %token LBRACKET RBRACKET PIPE ARROW COMMA EQUAL %token LPAREN RPAREN COLON SEMICOLON %token GLOBAL FIRST LAST BEFORE AFTER LEVEL LEFTA RIGHTA NONA @@ -108,8 +108,13 @@ vernac_extend: ; tactic_extend: -| TACTIC EXTEND IDENT tactic_level tactic_rules END - { TacticExt { tacext_name = $3; tacext_level = $4; tacext_rules = $5 } } +| TACTIC EXTEND IDENT tactic_deprecated tactic_level tactic_rules END + { TacticExt { tacext_name = $3; tacext_deprecated = $4; tacext_level = $5; tacext_rules = $6 } } +; + +tactic_deprecated: +| { None } +| DEPRECATED CODE { Some $2 } ; tactic_level: diff --git a/default.nix b/default.nix index d9317bccaf..6f759f41d1 100644 --- a/default.nix +++ b/default.nix @@ -23,8 +23,8 @@ { pkgs ? (import (fetchTarball { - url = "https://github.com/NixOS/nixpkgs/archive/060a98e9f4ad879492e48d63e887b0b6db26299e.tar.gz"; - sha256 = "1lzvp3md0hf6kp2bvc6dbzh40navlyd51qlns9wbkz6lqk3lgf6j"; + url = "https://github.com/NixOS/nixpkgs/archive/4477cf04b6779a537cdb5f0bd3dd30e75aeb4a3b.tar.gz"; + sha256 = "1i39wsfwkvj9yryj8di3jibpdg3b3j86ych7s9rb6z79k08yaaxc"; }) {}) , ocamlPackages ? pkgs.ocaml-ng.ocamlPackages_4_06 , buildIde ? true @@ -38,6 +38,18 @@ with pkgs; with stdenv.lib; +let dune = + overrideDerivation jbuilder (o: { + name = "dune-1.1.1"; + src = fetchFromGitHub { + owner = "ocaml"; + repo = "dune"; + rev = "1.1.1"; + sha256 = "0v2pnxpmqsvrvidpwxvbsypzhqfdnjs5crjp9y61qi8nyj8d75zw"; + }; + }); +in + stdenv.mkDerivation rec { name = "coq"; @@ -45,6 +57,7 @@ stdenv.mkDerivation rec { buildInputs = [ hostname python2 time # coq-makefile timing tools + dune ] ++ (with ocamlPackages; [ ocaml findlib camlp5_strict num ]) ++ optional buildIde ocamlPackages.lablgtk @@ -62,8 +75,8 @@ stdenv.mkDerivation rec { ++ [ ocamlPackages.ounit rsync which ] ) ++ optionals shell ( - [ jq curl git gnupg ] # Dependencies of the merging script - ++ (with ocamlPackages; [ merlin ocp-indent ocp-index ]) # Dev tools + [ jq curl gitFull gnupg ] # Dependencies of the merging script + ++ (with ocamlPackages; [ merlin ocp-indent ocp-index utop ]) # Dev tools ); src = @@ -71,7 +84,7 @@ stdenv.mkDerivation rec { else with builtins; filterSource (path: _: - !elem (baseNameOf path) [".git" "result" "bin" "_build_ci"]) ./.; + !elem (baseNameOf path) [".git" "result" "bin" "_build" "_build_ci"]) ./.; prefixKey = "-prefix "; diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md index 0b3e414513..85aaf317ef 100644 --- a/dev/doc/build-system.dune.md +++ b/dev/doc/build-system.dune.md @@ -39,6 +39,17 @@ In order to build a single package, you can do `dune build $PACKAGE.install`. Dune also provides targets for documentation and testing, see below. +## Developer shell + +You can create a developer shell with `dune utop $library`, where +`$library` can be any directory in the current workspace. For example, +`dune utop engine` or `dune utop plugins/ltac` will launch `utop` with +the right libraries already loaded. + +Note that you must invoke the `#rectypes;;` toplevel flag in order to +use Coq libraries. The provided `.ocamlinit` file does this +automatically. + ## Compositionality, developer and release modes. By default [in "developer mode"], Dune will compose all the packages diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index f7fd4b9146..e507a224c6 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -407,12 +407,11 @@ length, by writing .. coqtop:: in - Fixpoint concat (n:nat) (l:listn n) (m:nat) (l':listn m) {struct l} : - listn (n + m) := - match l in listn n, l' return listn (n + m) with - | niln, x => x - | consn n' a y, x => consn (n' + m) a (concat n' y m x) - end. + Check (fun n (a b: listn n) => + match a, b with + | niln, b0 => tt + | consn n' a y, bS => tt + end). we have a copy of :g:`b` in type :g:`listn 0` resp. :g:`listn (S n')`. diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index c0c4539564..23cbd76eda 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -325,6 +325,12 @@ Coercions and Modules This option makes it possible to recover the behavior of the versions of |Coq| prior to 8.3. +.. warn:: Coercion used but not in scope: @qualid. If you want to use this coercion, please Import the module that contains it. + + This warning is emitted when typechecking relies on a coercion + contained in a module that has not been explicitely imported. It helps + migrating code and stop relying on the option above. + Examples -------- diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 1e92d01125..f7a431ef29 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -26,7 +26,9 @@ Description of ``omega`` .. tacv:: romega :name: romega - To be documented. + .. deprecated:: 8.9 + + Use :tacn:`lia` instead. Arithmetical goals recognized by ``omega`` ------------------------------------------ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 241cdf5eea..62a482096c 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1345,8 +1345,8 @@ name of the variable (here :g:`n`) is chosen based on :g:`T`. changes in the goal, its use is strongly discouraged. .. tacv:: instantiate ( @num := @term ) in @ident -.. tacv:: instantiate ( @num := @term ) in ( Value of @ident ) -.. tacv:: instantiate ( @num := @term ) in ( Type of @ident ) +.. tacv:: instantiate ( @num := @term ) in ( value of @ident ) +.. tacv:: instantiate ( @num := @term ) in ( type of @ident ) These allow to refer respectively to existential variables occurring in a hypothesis or in the body or the type of a local definition. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index b46382dbbf..4c0e85bdd4 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -949,16 +949,25 @@ Interpretation scopes can include an interpretation for numerals and strings. However, this is only made possible at the Objective Caml level. -See :ref:`above <NotationSyntax>` for the syntax of notations including the -possibility to declare them in a given scope. Here is a typical example which -declares the notation for conjunction in the scope ``type_scope``. +.. cmd:: Declare Scope @scope + + This adds a new scope named :n:`@scope`. Note that the initial + state of Coq declares by default the following interpretation scopes: + ``core_scope``, ``type_scope``, ``function_scope``, ``nat_scope``, + ``bool_scope``, ``list_scope``, ``int_scope``, ``uint_scope``. + +The syntax to associate a notation to a scope is given +:ref:`above <NotationSyntax>`. Here is a typical example which declares the +notation for conjunction in the scope ``type_scope``. .. coqtop:: in Notation "A /\ B" := (and A B) : type_scope. .. note:: A notation not defined in a scope is called a *lonely* - notation. + notation. No example of lonely notations can be found in the + initial state of Coq though. + Global interpretation rules for notations ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ @@ -977,10 +986,6 @@ interpretation: otherwise said, only the order of lonely interpretations and opening of scopes matters, and not the declaration of interpretations within a scope). -The initial state of Coq declares three interpretation scopes and no -lonely notations. These scopes, in opening order, are ``core_scope``, -``type_scope`` and ``nat_scope``. - .. cmd:: Open Scope @scope The command to add a scope to the interpretation scope stack is @@ -9,7 +9,3 @@ (name vodeps) (deps tools/coq_dune.exe .vfiles.d)) ; (action (run coq_dune .vfiles.d)))) - -; Add custom flags here. Default developer profile is `dev` -(env - (dev (flags :standard -rectypes -w -9-27-50))) diff --git a/dune-project b/dune-project index b98bfa1013..6ce4ec4717 100644 --- a/dune-project +++ b/dune-project @@ -1,3 +1,3 @@ -(lang dune 1.0) +(lang dune 1.1) (name coq-devel) diff --git a/dune-workspace b/dune-workspace new file mode 100644 index 0000000000..682631e7dc --- /dev/null +++ b/dune-workspace @@ -0,0 +1,6 @@ +(lang dune 1.1) + +; Add custom flags here. Default developer profile is `dev` +(env + (dev (flags :standard -rectypes -w -9-27-50)) + (release (flags :standard -rectypes))) diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp index 07239e7af0..5943600b7c 100644 --- a/grammar/tacextend.mlp +++ b/grammar/tacextend.mlp @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(** WARNING: this file is deprecated; consider modifying coqpp instead. *) + (** Implementation of the TACTIC EXTEND macro. *) open Q_util diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 960beb8455..7044263b94 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -71,15 +71,15 @@ let insert_xml ?(mark = `INSERT) ?(tags = []) (buf : #GText.buffer_skel) msg = let rmark = `MARK (buf#create_mark buf#start_iter) in (* insert the string, but don't apply diff highlights to white space at the begin/end of line *) let rec insert_str tags s = + let etags = try List.hd !dtags :: tags with hd -> tags in try - let _ = Str.search_forward nl_white_regex s 0 in + let start = Str.search_forward nl_white_regex s 0 in + insert_with_tags buf mark rmark etags (String.sub s 0 start); insert_with_tags buf mark rmark tags (Str.matched_group 1 s); let mend = Str.match_end () in insert_str tags (String.sub s mend (String.length s - mend)) - with Not_found -> begin - let etags = try List.hd !dtags :: tags with hd -> tags in + with Not_found -> insert_with_tags buf mark rmark etags s - end in let rec insert tags = function | PCData s -> insert_str tags s @@ -328,15 +328,18 @@ let coqtop_path () = | None -> try let new_prog = System.get_toplevel_path "coqidetop" in - if Sys.file_exists new_prog then new_prog + (* The file exists or it is to be found by path *) + if Sys.file_exists new_prog || + CString.equal Filename.(basename new_prog) new_prog + then new_prog else let in_macos_bundle = Filename.concat (Filename.dirname new_prog) (Filename.concat "../Resources/bin" (Filename.basename new_prog)) in if Sys.file_exists in_macos_bundle then in_macos_bundle - else "coqidetop" - with Not_found -> "coqidetop" + else "coqidetop.opt" + with Not_found -> "coqidetop.opt" in file (* In win32, when a command-line is to be executed via cmd.exe diff --git a/interp/notation.ml b/interp/notation.ml index 55ead946cb..6b26f66100 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -98,21 +98,40 @@ let init_scope_map () = (**********************************************************************) (* Operations on scopes *) +let warn_undeclared_scope = + CWarnings.create ~name:"undeclared-scope" ~category:"deprecated" + (fun (scope) -> + strbrk "Declaring a scope implicitly is deprecated; use in advance an explicit " + ++ str "\"Declare Scope " ++ str scope ++ str ".\".") + let declare_scope scope = try let _ = String.Map.find scope !scope_map in () with Not_found -> -(* Flags.if_warn message ("Creating scope "^scope);*) scope_map := String.Map.add scope empty_scope !scope_map let error_unknown_scope sc = user_err ~hdr:"Notation" (str "Scope " ++ str sc ++ str " is not declared.") -let find_scope scope = +let find_scope ?(tolerant=false) scope = try String.Map.find scope !scope_map - with Not_found -> error_unknown_scope scope + with Not_found -> + if tolerant then + (* tolerant mode to be turn off after deprecation phase *) + begin + warn_undeclared_scope scope; + scope_map := String.Map.add scope empty_scope !scope_map; + empty_scope + end + else + error_unknown_scope scope + +let check_scope ?(tolerant=false) scope = + let _ = find_scope ~tolerant scope in () + +let ensure_scope scope = check_scope ~tolerant:true scope -let check_scope sc = let _ = find_scope sc in () +let find_scope scope = find_scope scope (* [sc] might be here a [scope_name] or a [delimiter] (now allowed after Open Scope) *) @@ -418,7 +437,7 @@ type prim_token_infos = { let cache_prim_token_interpretation (_,infos) = let sc = infos.pt_scope in let uid = infos.pt_uid in - declare_scope sc; + check_scope ~tolerant:true sc; prim_token_interp_infos := String.Map.add sc (infos.pt_required,infos.pt_uid) !prim_token_interp_infos; List.iter (fun r -> prim_token_uninterp_infos := diff --git a/interp/notation.mli b/interp/notation.mli index e5478eff48..6e59c0fd70 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -41,6 +41,9 @@ type scopes (** = [scope_name list] *) val declare_scope : scope_name -> unit +(* To be removed after deprecation phase *) +val ensure_scope : scope_name -> unit + val current_scopes : unit -> scopes (** Check where a scope is opened or not in a scope list, or in diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 7c00e40fb0..961036d3c5 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -269,7 +269,7 @@ let lam_subst_args subst args = let can_subst lam = match lam with | Lrel _ | Lvar _ | Lconst _ - | Lval _ | Lsort _ | Lind _ | Llam _ -> true + | Lval _ | Lsort _ | Lind _ -> true | _ -> false let rec simplify subst lam = diff --git a/lib/system.ml b/lib/system.ml index eef65a4e3d..902a4f2506 100644 --- a/lib/system.ml +++ b/lib/system.ml @@ -301,8 +301,11 @@ let with_time ~batch f x = Feedback.msg_info (str msg ++ fmt_time_difference tstart tend ++ str msg2); raise e +(* We use argv.[0] as we don't want to resolve symlinks *) let get_toplevel_path top = - let dir = Filename.dirname Sys.executable_name in + let open Filename in + let dir = if String.equal (basename Sys.argv.(0)) Sys.argv.(0) + then "" else dirname Sys.argv.(0) ^ dir_sep in let exe = if Sys.(os_type = "Win32" || os_type = "Cygwin") then ".exe" else "" in let eff = if Dynlink.is_native then ".opt" else ".byte" in - dir ^ Filename.dir_sep ^ top ^ eff ^ exe + dir ^ top ^ eff ^ exe diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v index ee7341a4a2..f1095fc9f1 100644 --- a/plugins/btauto/Algebra.v +++ b/plugins/btauto/Algebra.v @@ -1,4 +1,4 @@ -Require Import Bool PArith DecidableClass Omega ROmega. +Require Import Bool PArith DecidableClass Omega Lia. Ltac bool := repeat match goal with @@ -84,9 +84,9 @@ Ltac case_decide := match goal with let H := fresh "H" in define (@decide P D) b H; destruct b; try_decide | [ |- context [Pos.compare ?x ?y] ] => - destruct (Pos.compare_spec x y); try (exfalso; zify; romega) + destruct (Pos.compare_spec x y); try lia | [ X : context [Pos.compare ?x ?y] |- _ ] => - destruct (Pos.compare_spec x y); try (exfalso; zify; romega) + destruct (Pos.compare_spec x y); try lia end. Section Definitions. @@ -325,13 +325,13 @@ Qed. Lemma linear_le_compat : forall k l p, linear k p -> (k <= l)%positive -> linear l p. Proof. -intros k l p H; revert l; induction H; constructor; eauto; zify; romega. +intros k l p H; revert l; induction H; constructor; eauto; lia. Qed. Lemma linear_valid_incl : forall k p, linear k p -> valid k p. Proof. intros k p H; induction H; constructor; auto. -eapply valid_le_compat; eauto; zify; romega. +eapply valid_le_compat; eauto; lia. Qed. End Validity. @@ -417,13 +417,13 @@ Qed. Hint Extern 5 => match goal with | [ |- (Pos.max ?x ?y <= ?z)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (?z <= Pos.max ?x ?y)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (Pos.max ?x ?y < ?z)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | [ |- (?z < Pos.max ?x ?y)%positive ] => - apply Pos.max_case_strong; intros; zify; romega + apply Pos.max_case_strong; intros; lia | _ => zify; omega end. Hint Resolve Pos.le_max_r Pos.le_max_l. @@ -445,8 +445,8 @@ intros kl kr pl pr Hl Hr; revert kr pr Hr; induction Hl; intros kr pr Hr; simpl. now rewrite <- (Pos.max_id i); intuition. destruct (Pos.compare_spec i i0); subst; try case_decide; repeat (constructor; intuition). + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; auto. - + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; zify; romega. - + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; zify; romega. + + apply (valid_le_compat (Pos.max i0 i0)); [now auto|]; rewrite Pos.max_id; lia. + + apply (valid_le_compat (Pos.max (Pos.succ i0) (Pos.succ i0))); [now auto|]; rewrite Pos.max_id; lia. + apply (valid_le_compat (Pos.max (Pos.succ i) i0)); intuition. + apply (valid_le_compat (Pos.max i (Pos.succ i0))); intuition. } @@ -456,7 +456,7 @@ Lemma poly_mul_cst_valid_compat : forall k v p, valid k p -> valid k (poly_mul_c Proof. intros k v p H; induction H; simpl; [now auto|]. case_decide; [|now auto]. -eapply (valid_le_compat i); [now auto|zify; romega]. +eapply (valid_le_compat i); [now auto|lia]. Qed. Lemma poly_mul_mon_null_compat : forall i p, null (poly_mul_mon i p) -> null p. diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index d779951180..38600695dc 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -199,9 +199,9 @@ let pr_gen_place pr_id = function ConclLocation () -> Pp.mt () | HypLocation (id,InHyp) -> str "in " ++ pr_id id | HypLocation (id,InHypTypeOnly) -> - str "in (Type of " ++ pr_id id ++ str ")" + str "in (type of " ++ pr_id id ++ str ")" | HypLocation (id,InHypValueOnly) -> - str "in (Value of " ++ pr_id id ++ str ")" + str "in (value of " ++ pr_id id ++ str ")" let pr_loc_place _ _ _ = pr_gen_place (fun { CAst.v = id } -> Id.print id) let pr_place _ _ _ = pr_gen_place Id.print @@ -220,6 +220,14 @@ let interp_place ist gl p = let subst_place subst pl = pl +let warn_deprecated_instantiate_syntax = + CWarnings.create ~name:"deprecated-instantiate-syntax" ~category:"deprecated" + (fun (v,v',id) -> + let s = Id.to_string id in + Pp.strbrk + ("Syntax \"in (" ^ v ^ " of " ^ s ^ ")\" is deprecated; use \"in (" ^ v' ^ " of " ^ s ^ ")\".") + ) + ARGUMENT EXTEND hloc PRINTED BY pr_place INTERPRETED BY interp_place @@ -234,8 +242,14 @@ ARGUMENT EXTEND hloc | [ "in" ident(id) ] -> [ HypLocation ((CAst.make id),InHyp) ] | [ "in" "(" "Type" "of" ident(id) ")" ] -> - [ HypLocation ((CAst.make id),InHypTypeOnly) ] + [ warn_deprecated_instantiate_syntax ("Type","type",id); + HypLocation ((CAst.make id),InHypTypeOnly) ] | [ "in" "(" "Value" "of" ident(id) ")" ] -> + [ warn_deprecated_instantiate_syntax ("Value","value",id); + HypLocation ((CAst.make id),InHypValueOnly) ] +| [ "in" "(" "type" "of" ident(id) ")" ] -> + [ HypLocation ((CAst.make id),InHypTypeOnly) ] +| [ "in" "(" "value" "of" ident(id) ")" ] -> [ HypLocation ((CAst.make id),InHypValueOnly) ] END diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v index 51b99b9935..da86f4274d 100644 --- a/plugins/romega/ReflOmegaCore.v +++ b/plugins/romega/ReflOmegaCore.v @@ -8,6 +8,7 @@ *************************************************************************) Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base. +Declare Scope Int_scope. Delimit Scope Int_scope with I. (** * Abstract Integers. *) @@ -716,6 +717,7 @@ Inductive term : Set := | Topp : term -> term | Tvar : N -> term. +Declare Scope romega_scope. Bind Scope romega_scope with term. Delimit Scope romega_scope with term. Arguments Tint _%I. diff --git a/plugins/romega/g_romega.mlg b/plugins/romega/g_romega.mlg index c1ce30027e..ac4f30b1db 100644 --- a/plugins/romega/g_romega.mlg +++ b/plugins/romega/g_romega.mlg @@ -41,14 +41,22 @@ let romega_tactic unsafe l = (Tactics.intros) (total_reflexive_omega_tactic unsafe)) +let romega_depr = + Vernacinterp.mk_deprecation + ~since:(Some "8.9") + ~note:(Some "Use lia instead.") + () + } TACTIC EXTEND romega +DEPRECATED { romega_depr } | [ "romega" ] -> { romega_tactic false [] } | [ "unsafe_romega" ] -> { romega_tactic true [] } END TACTIC EXTEND romega' +DEPRECATED { romega_depr } | [ "romega" "with" ne_ident_list(l) ] -> { romega_tactic false (List.map Names.Id.to_string l) } | [ "romega" "with" "*" ] -> { romega_tactic false ["nat";"positive";"N";"Z"] } diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index d9e32dbbf8..ce115f564f 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -19,6 +19,7 @@ Section MakeFieldPol. (* Field elements : R *) Variable R:Type. +Declare Scope R_scope. Bind Scope R_scope with R. Delimit Scope R_scope with ring. Local Open Scope R_scope. @@ -94,6 +95,7 @@ Let rdistr_r := ARdistr_r Rsth Reqe ARth. (* Coefficients : C *) Variable C: Type. +Declare Scope C_scope. Bind Scope C_scope with C. Delimit Scope C_scope with coef. @@ -139,6 +141,7 @@ Let rpow_pow := pow_th.(rpow_pow_N). (* Polynomial expressions : (PExpr C) *) +Declare Scope PE_scope. Bind Scope PE_scope with PExpr. Delimit Scope PE_scope with poly. diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 523c7b02eb..1ca6227f25 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -79,8 +79,9 @@ Context {R:Type}`{Ring R}. | Z0 => 0 | Zneg p => -(gen_phiPOS p) end. - Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. - Local Open Scope ZMORPHISM. + Declare Scope ZMORPHISM. + Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. + Open Scope ZMORPHISM. Definition get_signZ z := match z with diff --git a/plugins/ssr/ssreflect.v b/plugins/ssr/ssreflect.v index b4144aa45e..460bdc6d23 100644 --- a/plugins/ssr/ssreflect.v +++ b/plugins/ssr/ssreflect.v @@ -86,6 +86,7 @@ Export SsrSyntax. (* recognize the expansion of the boolean if; using the default printer *) (* avoids a spurrious trailing %GEN_IF. *) +Declare Scope general_if_scope. Delimit Scope general_if_scope with GEN_IF. Notation "'if' c 'then' v1 'else' v2" := @@ -103,6 +104,7 @@ Notation "'if' c 'as' x 'return' t 'then' v1 'else' v2" := (* Force boolean interpretation of simple if expressions. *) +Declare Scope boolean_if_scope. Delimit Scope boolean_if_scope with BOOL_IF. Notation "'if' c 'return' t 'then' v1 'else' v2" := @@ -125,6 +127,7 @@ Open Scope boolean_if_scope. (* Non-ssreflect libraries that do not respect the form syntax (e.g., the Coq *) (* Lists library) should be loaded before ssreflect so that their notations *) (* do not mask all ssreflect forms. *) +Declare Scope form_scope. Delimit Scope form_scope with FORM. Open Scope form_scope. diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index fbe3b000fb..602fcfcab5 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -293,7 +293,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let c, cl, ucst = match_pat env p occ h cl in let gl = pf_merge_uc ucst gl in let c = EConstr.of_constr c in - let gl = try pf_unify_HO gl inf_t c with _ -> error gl c inf_t in + let gl = try pf_unify_HO gl inf_t c + with exn when CErrors.noncritical exn -> error gl c inf_t in cl, gl, post with | NoMatch | NoProgress -> @@ -302,7 +303,8 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let e = EConstr.of_constr e in let n, e, _, _ucst = pf_abs_evars gl (fst p, e) in let e, _, _, gl = pf_saturate ~beta:true gl e n in - let gl = try pf_unify_HO gl inf_t e with _ -> error gl e inf_t in + let gl = try pf_unify_HO gl inf_t e + with exn when CErrors.noncritical exn -> error gl e inf_t in cl, gl, post in let rec match_all concl gl patterns = diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 23cbf49c05..f23433f2f4 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -115,7 +115,8 @@ let newssrcongrtac arg ist gl = (* utils *) let fs gl t = Reductionops.nf_evar (project gl) t in let tclMATCH_GOAL (c, gl_c) proj t_ok t_fail gl = - match try Some (pf_unify_HO gl_c (pf_concl gl) c) with _ -> None with + match try Some (pf_unify_HO gl_c (pf_concl gl) c) + with exn when CErrors.noncritical exn -> None with | Some gl_c -> tclTHEN (Proofview.V82.of_tactic (convert_concl (fs gl_c c))) (t_ok (proj gl_c)) gl diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index b2d5143e36..99ff943e61 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -216,6 +216,7 @@ Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. +Declare Scope fun_scope. Delimit Scope fun_scope with FUN. Open Scope fun_scope. @@ -225,6 +226,7 @@ Notation "f ^~ y" := (fun x => f x y) Notation "@^~ x" := (fun f => f x) (at level 10, x at level 8, no associativity, format "@^~ x") : fun_scope. +Declare Scope pair_scope. Delimit Scope pair_scope with PAIR. Open Scope pair_scope. diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 30a998c6ce..20ea8b3667 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -291,7 +291,10 @@ let unif_EQ_args env sigma pa a = prof_unif_eq_args.profile (unif_EQ_args env sigma pa) a ;; -let unif_HO env ise p c = Evarconv.the_conv_x env p c ise +let unif_HO env ise p c = + try Evarconv.the_conv_x env p c ise + with Evarconv.UnableToUnify(ise, err) -> + raise Pretype_errors.(PretypeError(env,ise,CannotUnify(p,c,Some err))) let unif_HO_args env ise0 pa i ca = let n = Array.length pa in diff --git a/plugins/ssrmatching/ssrmatching.v b/plugins/ssrmatching/ssrmatching.v index 829ee05e11..9a53e1dd1a 100644 --- a/plugins/ssrmatching/ssrmatching.v +++ b/plugins/ssrmatching/ssrmatching.v @@ -11,9 +11,11 @@ Reserved Notation "( a 'as' b )" (at level 0). Reserved Notation "( a 'in' b 'in' c )" (at level 0). Reserved Notation "( a 'as' b 'in' c )" (at level 0). +Declare Scope ssrpatternscope. +Delimit Scope ssrpatternscope with pattern. + (* Notation to define shortcuts for the "X in t" part of a pattern. *) Notation "( X 'in' t )" := (_ : fun X => t) : ssrpatternscope. -Delimit Scope ssrpatternscope with pattern. (* Some shortcuts for recurrent "X in t" parts. *) Notation RHS := (X in _ = X)%pattern. diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 542fb5456c..332ecd2c91 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -16,7 +16,6 @@ open Constr open Libnames open Globnames open Nametab -open Environ open Libobject open Mod_subst @@ -118,6 +117,9 @@ let class_tab = let coercion_tab = ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t) +let coercions_in_scope = + ref Refset_env.empty + module ClPairOrd = struct type t = cl_index * cl_index @@ -131,12 +133,13 @@ module ClPairMap = Map.Make(ClPairOrd) let inheritance_graph = ref (ClPairMap.empty : inheritance_path ClPairMap.t) -let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph) +let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph, !coercions_in_scope) -let unfreeze (fcl,fco,fig) = +let unfreeze (fcl,fco,fig,in_scope) = class_tab:=fcl; coercion_tab:=fco; - inheritance_graph:=fig + inheritance_graph:=fig; + coercions_in_scope:=in_scope (* ajout de nouveaux "objets" *) @@ -316,16 +319,16 @@ let lookup_pattern_path_between env (s,t) = (* rajouter une coercion dans le graphe *) -let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = - ref (fun _ _ _ -> str "<a class path>") +let path_printer : ((Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref = + ref (fun _ -> str "<a class path>") let install_path_printer f = path_printer := f -let print_path env sigma x = !path_printer env sigma x +let print_path x = !path_printer x -let message_ambig env sigma l = +let message_ambig l = str"Ambiguous paths:" ++ spc () ++ - prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l + prlist_with_sep fnl print_path l (* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit coercion,source,target *) @@ -339,7 +342,7 @@ let different_class_params i = | CL_CONST c -> Global.is_polymorphic (ConstRef c) | _ -> false -let add_coercion_in_graph env sigma (ic,source,target) = +let add_coercion_in_graph (ic,source,target) = let old_inheritance_graph = !inheritance_graph in let ambig_paths = (ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in @@ -381,7 +384,7 @@ let add_coercion_in_graph env sigma (ic,source,target) = end; let is_ambig = match !ambig_paths with [] -> false | _ -> true in if is_ambig && not !Flags.quiet then - Feedback.msg_info (message_ambig env sigma !ambig_paths) + Feedback.msg_info (message_ambig !ambig_paths) type coercion = { coercion_type : coe_typ; @@ -426,7 +429,7 @@ let _ = optread = (fun () -> !automatically_import_coercions); optwrite = (:=) automatically_import_coercions } -let cache_coercion env sigma (_, c) = +let cache_coercion (_, c) = let () = add_class c.coercion_source in let () = add_class c.coercion_target in let is, _ = class_info c.coercion_source in @@ -439,15 +442,22 @@ let cache_coercion env sigma (_, c) = coe_param = c.coercion_params; } in let () = add_new_coercion c.coercion_type xf in - add_coercion_in_graph env sigma (xf,is,it) + add_coercion_in_graph (xf,is,it) let load_coercion _ o = if !automatically_import_coercions then - cache_coercion (Global.env ()) Evd.empty o + cache_coercion o + +let set_coercion_in_scope (_, c) = + let r = c.coercion_type in + coercions_in_scope := Refset_env.add r !coercions_in_scope let open_coercion i o = - if Int.equal i 1 && not !automatically_import_coercions then - cache_coercion (Global.env ()) Evd.empty o + if Int.equal i 1 then begin + set_coercion_in_scope o; + if not !automatically_import_coercions then + cache_coercion o + end let subst_coercion (subst, c) = let coe = subst_coe_typ subst c.coercion_type in @@ -492,8 +502,8 @@ let inCoercion : coercion -> obj = open_function = open_coercion; load_function = load_coercion; cache_function = (fun objn -> - let env = Global.env () in cache_coercion env Evd.empty objn - ); + set_coercion_in_scope objn; + cache_coercion objn); subst_function = subst_coercion; classify_function = classify_coercion; discharge_function = discharge_coercion } @@ -553,3 +563,6 @@ let hide_coercion coe = let coe_info = coercion_info coe in Some coe_info.coe_param else None + +let is_coercion_in_scope r = + Refset_env.mem r !coercions_in_scope diff --git a/pretyping/classops.mli b/pretyping/classops.mli index af00c0a8dc..7c4842c8ae 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -99,7 +99,7 @@ val lookup_pattern_path_between : (**/**) (* Crade *) val install_path_printer : - (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit + ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit (**/**) (** {6 This is for printing purpose } *) @@ -113,3 +113,5 @@ val coercions : unit -> coe_info_typ list (** [hide_coercion] returns the number of params to skip if the coercion must be hidden, [None] otherwise; it raises [Not_found] if not a coercion *) val hide_coercion : coe_typ -> int option + +val is_coercion_in_scope : GlobRef.t -> bool diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 5e3821edf1..e15c00f7dc 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -363,12 +363,20 @@ let saturate_evd env evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:true ~fail:false env evd +let warn_coercion_not_in_scope = + CWarnings.create ~name:"coercion-not-in-scope" ~category:"deprecated" + Pp.(fun r -> str "Coercion used but not in scope: " ++ + Nametab.pr_global_env Id.Set.empty r ++ str ". If you want to use " + ++ str "this coercion, please Import the module that contains it.") + (* Apply coercion path from p to hj; raise NoCoercion if not applicable *) let apply_coercion env sigma p hj typ_cl = try let j,t,evd = List.fold_left (fun (ja,typ_cl,sigma) i -> + if not (is_coercion_in_scope i.coe_value) then + warn_coercion_not_in_scope i.coe_value; let isid = i.coe_is_identity in let isproj = i.coe_is_projection in let sigma, c = new_global sigma i.coe_value in @@ -386,7 +394,6 @@ let apply_coercion env sigma p hj typ_cl = (hj,typ_cl,sigma) p in evd, j with NoCoercion as e -> raise e - | e when CErrors.noncritical e -> anomaly (Pp.str "apply_coercion.") (* Try to coerce to a funclass; raise NoCoercion if not possible *) let inh_app_fun_core env evd j = diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml index eb283a0220..be79b8b07d 100644 --- a/pretyping/inferCumulativity.ml +++ b/pretyping/inferCumulativity.ml @@ -99,7 +99,7 @@ let rec infer_fterm cv_pb infos variances hd stk = | FEvar ((_,args),e) -> let variances = infer_stack infos variances stk in infer_vect infos variances (Array.map (mk_clos e) args) - | FRel _ -> variances + | FRel _ -> infer_stack infos variances stk | FFlex fl -> let variances = infer_table_key infos variances fl in infer_stack infos variances stk diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 1810cc6588..9ed985195f 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -902,28 +902,28 @@ let inspect env sigma depth = open Classops -let print_coercion_value env sigma v = Printer.pr_global v.coe_value +let print_coercion_value v = Printer.pr_global v.coe_value let print_class i = let cl,_ = class_info_from_index i in pr_class cl -let print_path env sigma ((i,j),p) = +let print_path ((i,j),p) = hov 2 ( - str"[" ++ hov 0 (prlist_with_sep pr_semicolon (print_coercion_value env sigma) p) ++ + str"[" ++ hov 0 (prlist_with_sep pr_semicolon print_coercion_value p) ++ str"] : ") ++ print_class i ++ str" >-> " ++ print_class j let _ = Classops.install_path_printer print_path -let print_graph env sigma = - prlist_with_sep fnl (print_path env sigma) (inheritance_graph()) +let print_graph () = + prlist_with_sep fnl print_path (inheritance_graph()) let print_classes () = pr_sequence pr_class (classes()) -let print_coercions env sigma = - pr_sequence (print_coercion_value env sigma) (coercions()) +let print_coercions () = + pr_sequence print_coercion_value (coercions()) let index_of_class cl = try @@ -932,7 +932,7 @@ let index_of_class cl = user_err ~hdr:"index_of_class" (pr_class cl ++ spc() ++ str "not a defined class.") -let print_path_between env sigma cls clt = +let print_path_between cls clt = let i = index_of_class cls in let j = index_of_class clt in let p = @@ -943,7 +943,7 @@ let print_path_between env sigma cls clt = (str"No path between " ++ pr_class cls ++ str" and " ++ pr_class clt ++ str ".") in - print_path env sigma ((i,j),p) + print_path ((i,j),p) let print_canonical_projections env sigma = prlist_with_sep fnl diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 1668bce297..58606db019 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -12,7 +12,6 @@ open Names open Environ open Reductionops open Libnames -open Evd (** A Pretty-Printer for the Calculus of Inductive Constructions. *) @@ -40,10 +39,10 @@ val print_about : env -> Evd.evar_map -> qualid Constrexpr.or_by_notation -> val print_impargs : qualid Constrexpr.or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) -val print_graph : env -> evar_map -> Pp.t +val print_graph : unit -> Pp.t val print_classes : unit -> Pp.t -val print_coercions : env -> Evd.evar_map -> Pp.t -val print_path_between : env -> evar_map -> Classops.cl_typ -> Classops.cl_typ -> Pp.t +val print_coercions : unit -> Pp.t +val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t val print_canonical_projections : env -> Evd.evar_map -> Pp.t (** Pretty-printing functions for type classes and instances *) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 678c3ea3f7..d971c28a26 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -173,8 +173,8 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = const_entry_body = Future.chain ce.const_entry_body (fun (pt, _) -> pt, ()) } in let (cb, ctx), () = Future.force ce.const_entry_body in - let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in - cb, status, Evd.evar_universe_context univs' + let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in + cb, status, univs let refine_by_tactic env sigma ty tac = (** Save the initial side-effects to restore them afterwards. We set the diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 2170477938..85babd922b 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -168,7 +168,8 @@ let classify_vernac e = | VernacDeclareModuleType ({v=id},bl,_,_) -> VtSideff [id], if bl = [] then VtLater else VtNow (* These commands alter the parser *) - | VernacOpenCloseScope _ | VernacDelimiters _ | VernacBindScope _ + | VernacOpenCloseScope _ | VernacDeclareScope _ + | VernacDelimiters _ | VernacBindScope _ | VernacInfix _ | VernacNotation _ | VernacNotationAddFormat _ | VernacSyntaxExtension _ | VernacSyntacticDefinition _ diff --git a/test-suite/Makefile b/test-suite/Makefile index b8aac8b6f8..f5ec80bcfc 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -106,7 +106,8 @@ SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile unit-te PREREQUISITELOG = prerequisite/admit.v.log \ prerequisite/make_local.v.log prerequisite/make_notation.v.log \ - prerequisite/bind_univs.v.log + prerequisite/bind_univs.v.log prerequisite/module_bug8416.v.log \ + prerequisite/module_bug7192.v.log ####################################################################### # Phony targets diff --git a/test-suite/bugs/closed/7795.v b/test-suite/bugs/closed/7795.v new file mode 100644 index 0000000000..5db0f81cc5 --- /dev/null +++ b/test-suite/bugs/closed/7795.v @@ -0,0 +1,65 @@ + + +Definition fwd (b: bool) A (e2: A): A. Admitted. + +Ltac destruct_refinement_aux T := + let m := fresh "mres" in + let r := fresh "r" in + let P := fresh "P" in + pose T as m; + destruct m as [ r P ]. + +Ltac destruct_refinement := + match goal with + | |- context[proj1_sig ?T] => destruct_refinement_aux T + end. + +Ltac t_base := discriminate || destruct_refinement. + + +Inductive List (T: Type) := +| Cons_construct: T -> List T -> List T +| Nil_construct: List T. + +Definition t (T: Type): List T. Admitted. +Definition size (T: Type) (src: List T): nat. Admitted. +Definition filter1_rt1_type (T: Type): Type := { res: List T | false = true }. +Definition filter1 (T: Type): filter1_rt1_type T. Admitted. + +Definition hh_1: + forall T : Type, + (forall (T0 : Type), + False -> filter1_rt1_type T0) -> + False. +Admitted. + +Definition hh_2: + forall (T : Type), + filter1_rt1_type T -> + filter1_rt1_type T. +Admitted. + +Definition hh: + forall (T : Type) (f1 : forall (T0 : Type), False -> filter1_rt1_type T0), + fwd + (Nat.leb + (size T + (fwd false (List T) + (fwd false (List T) + (proj1_sig + (hh_2 T + (f1 T (hh_1 T f1))))))) 0) bool + false = true. +Admitted. + +Set Program Mode. (* removing this line prevents the bug *) +Obligation Tactic := repeat t_base. + +Goal + forall T (h17: T), + filter1 T = + exist + _ + (Nil_construct T) + (hh T (fun (T : Type) (_ : False) => filter1 T)). +Abort. diff --git a/test-suite/bugs/closed/8288.v b/test-suite/bugs/closed/8288.v new file mode 100644 index 0000000000..0350be9c06 --- /dev/null +++ b/test-suite/bugs/closed/8288.v @@ -0,0 +1,7 @@ +Set Universe Polymorphism. +Set Printing Universes. + +Set Polymorphic Inductive Cumulativity. + +Inductive foo := C : (forall A : Type -> Type, A Type) -> foo. +(* anomaly invalid subtyping relation *) diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index bd9240476f..b67ac4f0df 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -10,6 +10,8 @@ Arguments Nat.sub !n !m. About Nat.sub. Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := fun x => (f (fst x), g (snd x)). +Declare Scope foo_scope. +Declare Scope bar_scope. Delimit Scope foo_scope with F. Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never. About pf. diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index fe6c05c39e..adab324cf0 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -76,6 +76,7 @@ Open Scope nat_scope. Inductive znat : Set := Zpos (n : nat) | Zneg (m : nat). Coercion Zpos: nat >-> znat. +Declare Scope znat_scope. Delimit Scope znat_scope with znat. Open Scope znat_scope. diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out index 34f44cd246..3f4d5ef58c 100644 --- a/test-suite/output/PrintAssumptions.out +++ b/test-suite/output/PrintAssumptions.out @@ -20,3 +20,5 @@ Axioms: M.foo : False Closed under the global context Closed under the global context +Closed under the global context +Closed under the global context diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v index ea1ab63786..3d4dfe603d 100644 --- a/test-suite/output/PrintAssumptions.v +++ b/test-suite/output/PrintAssumptions.v @@ -137,3 +137,13 @@ Module F (X : T). End F. End SUBMODULES. + +(* Testing a variant of #7192 across files *) +(* This was missing in the original fix to #7192 *) +Require Import module_bug7192. +Print Assumptions M7192.D.f. + +(* Testing reporting assumptions from modules in files *) +(* A regression introduced in the original fix to #7192 was missing implementations *) +Require Import module_bug8416. +Print Assumptions M8416.f. diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 6f41b2fcf9..926114a1e1 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -48,6 +48,12 @@ Type@{Top.17} -> Type@{v} -> Type@{u} (* u Top.17 v |= *) foo is universe polymorphic +Type@{i} -> Type@{j} + : Type@{max(i+1,j+1)} +(* {j i} |= *) + = Type@{i} -> Type@{j} + : Type@{max(i+1,j+1)} +(* {j i} |= *) Monomorphic mono = Type@{mono.u} : Type@{mono.u+1} (* {mono.u} |= *) @@ -149,24 +155,24 @@ inmod@{u} -> Type@{v} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i Top.44 Top.45} : Type@{Top.44} -> Type@{i} -(* i Top.44 Top.45 |= *) +axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i} +(* i Top.48 Top.49 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo -axbar@{i Top.44 Top.45} : Type@{Top.45} -> Type@{i} -(* i Top.44 Top.45 |= *) +axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i} +(* i Top.48 Top.49 |= *) axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axbar -axfoo' : Type@{Top.47} -> Type@{axbar'.i} +axfoo' : Type@{Top.51} -> Type@{axbar'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo' -axbar' : Type@{Top.47} -> Type@{axbar'.i} +axbar' : Type@{Top.51} -> Type@{axbar'.i} axbar' is not universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index c6efc240a6..f806a9f4f7 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -30,6 +30,11 @@ Unset Strict Universe Declaration. order of appearance. *) Definition foo@{u +} := Type -> Type@{v} -> Type@{u}. Print foo. + +Check Type@{i} -> Type@{j}. + +Eval cbv in Type@{i} -> Type@{j}. + Set Strict Universe Declaration. (* Binders even work with monomorphic definitions! *) diff --git a/test-suite/prerequisite/module_bug7192.v b/test-suite/prerequisite/module_bug7192.v new file mode 100644 index 0000000000..82cfe560af --- /dev/null +++ b/test-suite/prerequisite/module_bug7192.v @@ -0,0 +1,9 @@ +(* Variant of #7192 to be tested in a file requiring this file *) +(* #7192 is about Print Assumptions not entering implementation of submodules *) + +Definition a := True. +Module Type B. Axiom f : Prop. End B. +Module Type C. Declare Module D : B. End C. +Module M7192: C. + Module D <: B. Definition f := a. End D. +End M7192. diff --git a/test-suite/prerequisite/module_bug8416.v b/test-suite/prerequisite/module_bug8416.v new file mode 100644 index 0000000000..70f43d132a --- /dev/null +++ b/test-suite/prerequisite/module_bug8416.v @@ -0,0 +1,2 @@ +Module Type A. Axiom f : True. End A. +Module M8416 : A. Definition f := I. End M8416. diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v index 66a82008d8..42af3583d4 100644 --- a/theories/Bool/Bool.v +++ b/theories/Bool/Bool.v @@ -757,6 +757,8 @@ Qed. with lazy behavior (for vm_compute) *) (*****************************************) +Declare Scope lazy_bool_scope. + Notation "a &&& b" := (if a then b else false) (at level 40, left associativity) : lazy_bool_scope. Notation "a ||| b" := (if a then true else b) diff --git a/theories/Classes/CEquivalence.v b/theories/Classes/CEquivalence.v index 03e611f549..c376efef2e 100644 --- a/theories/Classes/CEquivalence.v +++ b/theories/Classes/CEquivalence.v @@ -35,6 +35,8 @@ Definition equiv `{Equivalence A R} : crelation A := R. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) +Declare Scope equiv_scope. + Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope. Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope. diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v index 09b35ca75d..97510578ae 100644 --- a/theories/Classes/CMorphisms.v +++ b/theories/Classes/CMorphisms.v @@ -87,6 +87,7 @@ Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances. (** Notations reminiscent of the old syntax for declaring morphisms. *) +Declare Scope signature_scope. Delimit Scope signature_scope with signature. Module ProperNotations. diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 5217aedb88..516ea12099 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -35,6 +35,8 @@ Definition equiv `{Equivalence A R} : relation A := R. (** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *) +Declare Scope equiv_scope. + Notation " x === y " := (equiv x y) (at level 70, no associativity) : equiv_scope. Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) : equiv_scope. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 1858ba76ae..001b7dfdfd 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -88,6 +88,7 @@ Hint Extern 2 (ProperProxy ?R _) => not_evar R; class_apply @proper_proper_proxy : typeclass_instances. (** Notations reminiscent of the old syntax for declaring morphisms. *) +Declare Scope signature_scope. Delimit Scope signature_scope with signature. Module ProperNotations. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 2ab3af2029..86a3a88be9 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -357,6 +357,8 @@ Definition predicate_implication {l : Tlist} := (** Notations for pointwise equivalence and implication of predicates. *) +Declare Scope predicate_scope. + Infix "<∙>" := predicate_equivalence (at level 95, no associativity) : predicate_scope. Infix "-∙>" := predicate_implication (at level 70, right associativity) : predicate_scope. diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v index 3485b9c68d..b0d1824827 100644 --- a/theories/FSets/FMapAVL.v +++ b/theories/FSets/FMapAVL.v @@ -25,6 +25,7 @@ Unset Strict Implicit. (** Notations and helper lemma about pairs *) +Declare Scope pair_scope. Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v index 3452967821..c0db8646c7 100644 --- a/theories/FSets/FMapFullAVL.v +++ b/theories/FSets/FMapFullAVL.v @@ -27,7 +27,7 @@ *) -Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL ROmega. +Require Import FunInd Recdef FMapInterface FMapList ZArith Int FMapAVL Lia. Set Implicit Arguments. Unset Strict Implicit. @@ -39,7 +39,7 @@ Import Raw.Proofs. Local Open Scope pair_scope. Local Open Scope Int_scope. -Ltac omega_max := i2z_refl; romega with Z. +Ltac omega_max := i2z_refl; lia. Section Elt. Variable elt : Type. @@ -697,7 +697,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <: end. Proof. intros; unfold cardinal_e_2; simpl; - abstract (do 2 rewrite cons_cardinal_e; romega with * ). + abstract (do 2 rewrite cons_cardinal_e; lia ). Defined. Definition Cmp c := diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 1e6843d511..76c39f275d 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -37,8 +37,8 @@ Inductive bool : Set := Add Printing If bool. +Declare Scope bool_scope. Delimit Scope bool_scope with bool. - Bind Scope bool_scope with bool. (** Basic boolean operators *) @@ -136,6 +136,7 @@ Inductive nat : Set := | O : nat | S : nat -> nat. +Declare Scope nat_scope. Delimit Scope nat_scope with nat. Bind Scope nat_scope with nat. Arguments S _%nat. @@ -228,10 +229,13 @@ Inductive list (A : Type) : Type := Arguments nil {A}. Arguments cons {A} a l. -Infix "::" := cons (at level 60, right associativity) : list_scope. + +Declare Scope list_scope. Delimit Scope list_scope with list. Bind Scope list_scope with list. +Infix "::" := cons (at level 60, right associativity) : list_scope. + Local Open Scope list_scope. Definition length (A : Type) : list A -> nat := diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 1ff00ec11c..537400fb05 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -42,8 +42,11 @@ Notation zero := (D0 Nil). Inductive int := Pos (d:uint) | Neg (d:uint). +Declare Scope dec_uint_scope. Delimit Scope dec_uint_scope with uint. Bind Scope dec_uint_scope with uint. + +Declare Scope dec_int_scope. Delimit Scope dec_int_scope with int. Bind Scope dec_int_scope with int. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 72073bb4f6..8f8e639187 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -108,13 +108,17 @@ End IfNotations. (** Scopes *) -Delimit Scope type_scope with type. -Delimit Scope function_scope with function. +Declare Scope core_scope. Delimit Scope core_scope with core. -Bind Scope type_scope with Sortclass. +Declare Scope function_scope. +Delimit Scope function_scope with function. Bind Scope function_scope with Funclass. +Declare Scope type_scope. +Delimit Scope type_scope with type. +Bind Scope type_scope with Sortclass. + Open Scope core_scope. Open Scope function_scope. Open Scope type_scope. diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index b6afba29a0..db8857df64 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -697,7 +697,7 @@ End Choice_lemmas. Section Dependent_choice_lemmas. - Variables X : Set. + Variable X : Set. Variable R : X -> X -> Prop. Lemma dependent_choice : diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v index b966f217aa..aec88f93bf 100644 --- a/theories/MSets/MSetAVL.v +++ b/theories/MSets/MSetAVL.v @@ -340,6 +340,8 @@ Functional Scheme union_ind := Induction for union Sort Prop. (** Notations and helper lemma about pairs and triples *) +Declare Scope pair_scope. + Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. Notation "t #l" := (t_left t) (at level 9, format "t '#l'") : pair_scope. diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index 3ba9d1f5ed..7b6740e94b 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -23,6 +23,7 @@ Inductive positive : Set := | xO : positive -> positive | xH : positive. +Declare Scope positive_scope. Delimit Scope positive_scope with positive. Bind Scope positive_scope with positive. Arguments xO _%positive. @@ -37,6 +38,7 @@ Inductive N : Set := | N0 : N | Npos : positive -> N. +Declare Scope N_scope. Delimit Scope N_scope with N. Bind Scope N_scope with N. Arguments Npos _%positive. @@ -53,6 +55,7 @@ Inductive Z : Set := | Zpos : positive -> Z | Zneg : positive -> Z. +Declare Scope Z_scope. Delimit Scope Z_scope with Z. Bind Scope Z_scope with Z. Arguments Zpos _%positive. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index ec480bb1eb..4a1f24b95e 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -21,7 +21,7 @@ Require Import Znumtheory. Require Import Zgcd_alt. Require Import Zpow_facts. Require Import CyclicAxioms. -Require Import ROmega. +Require Import Lia. Local Open Scope nat_scope. Local Open Scope int31_scope. @@ -1237,7 +1237,7 @@ Section Int31_Specs. destruct (Z_lt_le_dec (X+Y) wB). contradict H1; auto using Zmod_small with zarith. rewrite <- (Z_mod_plus_full (X+Y) (-1) wB). - rewrite Zmod_small; romega. + rewrite Zmod_small; lia. generalize (Z.compare_eq ((X+Y) mod wB) (X+Y)); intros Heq. destruct Z.compare; intros; @@ -1261,7 +1261,7 @@ Section Int31_Specs. destruct (Z_lt_le_dec (X+Y+1) wB). contradict H1; auto using Zmod_small with zarith. rewrite <- (Z_mod_plus_full (X+Y+1) (-1) wB). - rewrite Zmod_small; romega. + rewrite Zmod_small; lia. generalize (Z.compare_eq ((X+Y+1) mod wB) (X+Y+1)); intros Heq. destruct Z.compare; intros; @@ -1299,8 +1299,8 @@ Section Int31_Specs. unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros. destruct (Z_lt_le_dec (X-Y) 0). rewrite <- (Z_mod_plus_full (X-Y) 1 wB). - rewrite Zmod_small; romega. - contradict H1; apply Zmod_small; romega. + rewrite Zmod_small; lia. + contradict H1; apply Zmod_small; lia. generalize (Z.compare_eq ((X-Y) mod wB) (X-Y)); intros Heq. destruct Z.compare; intros; @@ -1318,8 +1318,8 @@ Section Int31_Specs. unfold interp_carry; rewrite phi_phi_inv, Z.compare_eq_iff; intros. destruct (Z_lt_le_dec (X-Y-1) 0). rewrite <- (Z_mod_plus_full (X-Y-1) 1 wB). - rewrite Zmod_small; romega. - contradict H1; apply Zmod_small; romega. + rewrite Zmod_small; lia. + contradict H1; apply Zmod_small; lia. generalize (Z.compare_eq ((X-Y-1) mod wB) (X-Y-1)); intros Heq. destruct Z.compare; intros; @@ -1356,7 +1356,7 @@ Section Int31_Specs. change [|1|] with 1; change [|0|] with 0. rewrite <- (Z_mod_plus_full (0-[|x|]) 1 wB). rewrite Zminus_mod_idemp_l. - rewrite Zmod_small; generalize (phi_bounded x); romega. + rewrite Zmod_small; generalize (phi_bounded x); lia. Qed. Lemma spec_pred_c : forall x, [-|sub31c x 1|] = [|x|] - 1. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index 39af62c32f..77ab624ca5 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -15,8 +15,6 @@ Require Import Wf_nat. Require Export ZArith. Require Export DoubleType. -Declare ML Module "int31_syntax_plugin". - (** * 31-bit integers *) (** This file contains basic definitions of a 31-bit integer @@ -50,6 +48,8 @@ Inductive int31 : Type := I31 : digits31 int31. Register digits as int31 bits in "coq_int31" by True. Register int31 as int31 type in "coq_int31" by True. +Declare Scope int31_scope. +Declare ML Module "int31_syntax_plugin". Delimit Scope int31_scope with int31. Bind Scope int31_scope with int31. Local Open Scope int31_scope. diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index d7f25a6613..a70ecd19d8 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -13,7 +13,7 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. (** * Euclidean Division for integers, Euclid convention We use here the "usual" formulation of the Euclid Theorem - [forall a b, b<>0 -> exists b q, a = b*q+r /\ 0 < r < |b| ] + [forall a b, b<>0 -> exists r q, a = b*q+r /\ 0 <= r < |b| ] The outcome of the modulo function is hence always positive. This corresponds to convention "E" in the following paper: @@ -46,6 +46,7 @@ Module ZEuclidProp (** We put notations in a scope, to avoid warnings about redefinitions of notations *) + Declare Scope euclid. Infix "/" := D.div : euclid. Infix "mod" := D.modulo : euclid. Local Open Scope euclid. diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v index 4b2d5c13b5..995d96b314 100644 --- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v +++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v @@ -13,15 +13,18 @@ Require Import NSub ZAxioms. Require Export Ring. +Declare Scope pair_scope. +Local Open Scope pair_scope. + Notation "s #1" := (fst s) (at level 9, format "s '#1'") : pair_scope. Notation "s #2" := (snd s) (at level 9, format "s '#2'") : pair_scope. -Local Open Scope pair_scope. Module ZPairsAxiomsMod (Import N : NAxiomsMiniSig) <: ZAxiomsMiniSig. Module Import NProp. Include NSubProp N. End NProp. +Declare Scope NScope. Delimit Scope NScope with N. Bind Scope NScope with N.t. Infix "==" := N.eq (at level 70) : NScope. @@ -73,6 +76,7 @@ Definition max (n m : t) : t := (max (n#1 + m#2) (m#1 + n#2), n#2 + m#2). End Z. +Declare Scope ZScope. Delimit Scope ZScope with Z. Bind Scope ZScope with Z.t. Infix "==" := Z.eq (at level 70) : ZScope. diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index 3d0c005fd1..acebfcf1d2 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -220,8 +220,10 @@ End NZDomainProp. Module NZOfNat (Import NZ:NZDomainSig'). Definition ofnat (n : nat) : t := (S^n) 0. -Notation "[ n ]" := (ofnat n) (at level 7) : ofnat. + +Declare Scope ofnat. Local Open Scope ofnat. +Notation "[ n ]" := (ofnat n) (at level 7) : ofnat. Lemma ofnat_zero : [O] == 0. Proof. diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index f55093ed48..c2316689fc 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -28,6 +28,8 @@ Definition compose {A B C} (g : B -> C) (f : A -> B) := Hint Unfold compose. +Declare Scope program_scope. + Notation " g ∘ f " := (compose g f) (at level 40, left associativity) : program_scope. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index bc83881849..edbae6534a 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -326,7 +326,7 @@ Ltac program_solve_wf := Create HintDb program discriminated. -Ltac program_simpl := program_simplify ; try typeclasses eauto with program ; try program_solve_wf. +Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; try program_solve_wf. Obligation Tactic := program_simpl. diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 78c36dc7d1..c51cacac68 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -20,12 +20,13 @@ Notation "{ ( x , y ) : A | P }" := (sig (fun anonymous : A => let (x,y) := anonymous in P)) (x ident, y ident, at level 10) : type_scope. +Declare Scope program_scope. +Delimit Scope program_scope with prg. + (** Generates an obligation to prove False. *) Notation " ! " := (False_rect _ _) : program_scope. -Delimit Scope program_scope with prg. - (** Abbreviation for first projection and hiding of proofs of subset objects. *) Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : program_scope. diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v index 35706e7fa2..139c4bf432 100644 --- a/theories/QArith/QArith_base.v +++ b/theories/QArith/QArith_base.v @@ -18,6 +18,7 @@ Require Export Morphisms Setoid Bool. Record Q : Set := Qmake {Qnum : Z; Qden : positive}. +Declare Scope Q_scope. Delimit Scope Q_scope with Q. Bind Scope Q_scope with Q. Arguments Qmake _%Z _%positive. diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index 1510a7b825..81c318138e 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -18,6 +18,7 @@ Require Import Eqdep_dec. Record Qc : Set := Qcmake { this :> Q ; canon : Qred this = this }. +Declare Scope Qc_scope. Delimit Scope Qc_scope with Qc. Bind Scope Qc_scope with Qc. Arguments Qcmake this%Q _. diff --git a/theories/Reals/Ranalysis1.v b/theories/Reals/Ranalysis1.v index 36ac738ca6..9f8039ec9d 100644 --- a/theories/Reals/Ranalysis1.v +++ b/theories/Reals/Ranalysis1.v @@ -28,6 +28,7 @@ Definition div_real_fct (a:R) f (x:R) : R := a / f x. Definition comp f1 f2 (x:R) : R := f1 (f2 x). Definition inv_fct f (x:R) : R := / f x. +Declare Scope Rfun_scope. Delimit Scope Rfun_scope with F. Arguments plus_fct (f1 f2)%F x%R. diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v index 6019d4faf1..a2818371e9 100644 --- a/theories/Reals/Raxioms.v +++ b/theories/Reals/Raxioms.v @@ -14,6 +14,7 @@ Require Export ZArith_base. Require Export Rdefinitions. +Declare Scope R_scope. Local Open Scope R_scope. (*********************************************************) diff --git a/theories/Reals/Rdefinitions.v b/theories/Reals/Rdefinitions.v index 857b4ec33b..932fcddaf5 100644 --- a/theories/Reals/Rdefinitions.v +++ b/theories/Reals/Rdefinitions.v @@ -12,12 +12,15 @@ (** Definitions for the axiomatization *) (*********************************************************) -Declare ML Module "r_syntax_plugin". Require Export ZArith_base. Parameter R : Set. -(* Declare Scope positive_scope with Key R *) +(* Declare primitive numeral notations for Scope R_scope *) +Declare Scope R_scope. +Declare ML Module "r_syntax_plugin". + +(* Declare Scope R_scope with Key R *) Delimit Scope R_scope with R. (* Automatically open scope R_scope for arguments of type R *) diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v index 31a7fb8ad6..3f676c1888 100644 --- a/theories/Strings/Ascii.v +++ b/theories/Strings/Ascii.v @@ -13,7 +13,6 @@ Adapted to Coq V8 by the Coq Development Team *) Require Import Bool BinPos BinNat PeanoNat Nnat. -Declare ML Module "ascii_syntax_plugin". (** * Definition of ascii characters *) @@ -21,6 +20,8 @@ Declare ML Module "ascii_syntax_plugin". Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool). +Declare Scope char_scope. +Declare ML Module "ascii_syntax_plugin". Delimit Scope char_scope with char. Bind Scope char_scope with ascii. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index be9a10c6dc..b27474ef25 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -15,7 +15,6 @@ Require Import Arith. Require Import Ascii. Require Import Bool. -Declare ML Module "string_syntax_plugin". (** *** Definition of strings *) @@ -25,6 +24,8 @@ Inductive string : Set := | EmptyString : string | String : ascii -> string -> string. +Declare Scope string_scope. +Declare ML Module "string_syntax_plugin". Delimit Scope string_scope with string. Bind Scope string_scope with string. Local Open Scope string_scope. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 87df6b479d..60c64d306b 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -132,6 +132,7 @@ Module OrderedTypeFacts (Import O: OrderedType'). Module OrderTac := OT_to_OrderTac O. Ltac order := OrderTac.order. + Declare Scope order. Notation "x <= y" := (~lt y x) : order. Infix "?=" := compare (at level 70, no associativity) : order. diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v index ba3e411091..390ca78c0e 100644 --- a/theories/Vectors/VectorDef.v +++ b/theories/Vectors/VectorDef.v @@ -305,6 +305,7 @@ Eval cbv delta beta in fold_right (fun h H => Datatypes.cons h H) v Datatypes.ni End VECTORLIST. Module VectorNotations. +Declare Scope vector_scope. Delimit Scope vector_scope with vector. Notation "[ ]" := [] (format "[ ]") : vector_scope. Notation "h :: t" := (h :: t) (at level 60, right associativity) diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 2f3bf9a32a..1e35370d29 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -17,6 +17,7 @@ *) Require Import BinInt. +Declare Scope Int_scope. Delimit Scope Int_scope with I. Local Open Scope Int_scope. diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index e93ebb1ad5..0c9aca2657 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Import Nnat ZArith_base ROmega ZArithRing Zdiv Morphisms. +Require Import Nnat ZArith_base Lia ZArithRing Zdiv Morphisms. Local Open Scope Z_scope. @@ -129,33 +129,33 @@ Qed. Theorem Zrem_lt_pos a b : 0<=a -> b<>0 -> 0 <= Z.rem a b < Z.abs b. Proof. intros; generalize (Z.rem_nonneg a b) (Z.rem_bound_abs a b); - romega with *. + lia. Qed. Theorem Zrem_lt_neg a b : a<=0 -> b<>0 -> -Z.abs b < Z.rem a b <= 0. Proof. intros; generalize (Z.rem_nonpos a b) (Z.rem_bound_abs a b); - romega with *. + lia. Qed. Theorem Zrem_lt_pos_pos a b : 0<=a -> 0<b -> 0 <= Z.rem a b < b. Proof. - intros; generalize (Zrem_lt_pos a b); romega with *. + intros; generalize (Zrem_lt_pos a b); lia. Qed. Theorem Zrem_lt_pos_neg a b : 0<=a -> b<0 -> 0 <= Z.rem a b < -b. Proof. - intros; generalize (Zrem_lt_pos a b); romega with *. + intros; generalize (Zrem_lt_pos a b); lia. Qed. Theorem Zrem_lt_neg_pos a b : a<=0 -> 0<b -> -b < Z.rem a b <= 0. Proof. - intros; generalize (Zrem_lt_neg a b); romega with *. + intros; generalize (Zrem_lt_neg a b); lia. Qed. Theorem Zrem_lt_neg_neg a b : a<=0 -> b<0 -> b < Z.rem a b <= 0. Proof. - intros; generalize (Zrem_lt_neg a b); romega with *. + intros; generalize (Zrem_lt_neg a b); lia. Qed. @@ -171,12 +171,12 @@ Lemma Remainder_equiv : forall a b r, Remainder a b r <-> Remainder_alt a b r. Proof. unfold Remainder, Remainder_alt; intuition. - - romega with *. - - romega with *. - - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; romega. + - lia. + - lia. + - rewrite <-(Z.mul_opp_opp). apply Z.mul_nonneg_nonneg; lia. - assert (0 <= Z.sgn r * Z.sgn a). { rewrite <-Z.sgn_mul, Z.sgn_nonneg; auto. } - destruct r; simpl Z.sgn in *; romega with *. + destruct r; simpl Z.sgn in *; lia. Qed. Theorem Zquot_mod_unique_full a b q r : @@ -185,7 +185,7 @@ Proof. destruct 1 as [(H,H0)|(H,H0)]; intros. apply Zdiv_mod_unique with b; auto. apply Zrem_lt_pos; auto. - romega with *. + lia. rewrite <- H1; apply Z.quot_rem'. rewrite <- (Z.opp_involutive a). @@ -193,7 +193,7 @@ Proof. generalize (Zdiv_mod_unique b (-q) (-a÷b) (-r) (Z.rem (-a) b)). generalize (Zrem_lt_pos (-a) b). rewrite <-Z.quot_rem', Z.mul_opp_r, <-Z.opp_add_distr, <-H1. - romega with *. + lia. Qed. Theorem Zquot_unique_full a b q r : diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml index c89c78c8ec..ab60920fbc 100644 --- a/tools/coq_dune.ml +++ b/tools/coq_dune.ml @@ -80,6 +80,7 @@ module Aux = struct module DirMap = Map.Make(DirOrd) (* Functions available in newer OCaml versions *) + (* Taken from the OCaml std library (c) INRIA / LGPL-2.1 *) module Legacy = struct (* Slower version of DirMap.update, waiting for OCaml 4.06.0 *) @@ -103,6 +104,29 @@ module Aux = struct end done; sub s 0 !j :: !r + + (* Available in OCaml >= 4.04 *) + let is_dir_sep = match Sys.os_type with + | "Win32" -> fun s i -> s.[i] = '\\' + | _ -> fun s i -> s.[i] = '/' + + let extension_len name = + let rec check i0 i = + if i < 0 || is_dir_sep name i then 0 + else if name.[i] = '.' then check i0 (i - 1) + else String.length name - i0 + in + let rec search_dot i = + if i < 0 || is_dir_sep name i then 0 + else if name.[i] = '.' then check i (i - 1) + else search_dot (i - 1) + in + search_dot (String.length name - 1) + + let remove_extension name = + let l = extension_len name in + if l = 0 then name else String.sub name 0 (String.length name - l) + end let add_map_list key elem map = @@ -181,18 +205,18 @@ let pp_vo_dep dir fmt vo = (* Correct path from global to local "theories/Init/Decimal.vo" -> "../../theories/Init/Decimal.vo" *) let deps = List.map (fun s -> sdir ^ s) (edep @ vo.deps) in (* The source file is also corrected as we will call coqtop from the top dir *) - let source = String.concat "/" dir ^ "/" ^ Filename.(remove_extension vo.target) ^ ".v" in + let source = String.concat "/" dir ^ "/" ^ Legacy.(remove_extension vo.target) ^ ".v" in (* The final build rule *) let action = sprintf "(chdir %%{project_root} (run coqtop -boot %s %s -compile %s))" eflag cflag source in pp_rule fmt [vo.target] deps action let pp_ml4_dep _dir fmt ml = - let target = Filename.(remove_extension ml) ^ ".ml" in + let target = Legacy.(remove_extension ml) ^ ".ml" in let ml4_rule = "(run coqp5 -loc loc -impl %{pp-file} -o %{targets})" in pp_rule fmt [target] [ml] ml4_rule let pp_mlg_dep _dir fmt ml = - let target = Filename.(remove_extension ml) ^ ".ml" in + let target = Legacy.(remove_extension ml) ^ ".ml" in let ml4_rule = "(run coqpp %{pp-file})" in pp_rule fmt [target] [ml] ml4_rule diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 765f962e99..e5d2382e46 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -70,7 +70,7 @@ let rec fields_of_functor f subs mp0 args = function let rec lookup_module_in_impl mp = match mp with - | MPfile _ -> raise Not_found + | MPfile _ -> Global.lookup_module mp | MPbound _ -> assert false | MPdot (mp',lab') -> if ModPath.equal mp' (Global.current_modpath ()) then diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 74516e320c..44c0159d1b 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -846,6 +846,10 @@ GRAMMAR EXTEND Gram info = hint_info -> { VernacInstance (true, snd namesup, (fst namesup, expl, t), None, info) } + (* Should be in syntax, but camlp5 would not factorize *) + | IDENT "Declare"; IDENT "Scope"; sc = IDENT -> + { VernacDeclareScope sc } + (* System directory *) | IDENT "Pwd" -> { VernacChdir None } | IDENT "Cd" -> { VernacChdir None } @@ -1141,8 +1145,8 @@ GRAMMAR EXTEND Gram l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> { l } | -> { [] } ] -> { VernacSyntaxExtension (false, (s,l)) } - (* "Print" "Grammar" should be here but is in "command" entry in order - to factorize with other "Print"-based vernac entries *) + (* "Print" "Grammar" and "Declare" "Scope" should be here but are in "command" entry in order + to factorize with other "Print"-based or "Declare"-based vernac entries *) ] ] ; only_parsing: diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index d66a121437..2e5e11bb09 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1306,8 +1306,18 @@ type notation_obj = { notobj_notation : notation * notation_location; } -let load_notation _ (_, nobj) = - Option.iter Notation.declare_scope nobj.notobj_scope +let load_notation_common silently_define_scope_if_undefined _ (_, nobj) = + (* When the default shall be to require that a scope already exists *) + (* the call to ensure_scope will have to be removed *) + if silently_define_scope_if_undefined then + (* Don't warn if the scope is not defined: *) + (* there was already a warning at "cache" time *) + Option.iter Notation.declare_scope nobj.notobj_scope + else + Option.iter Notation.ensure_scope nobj.notobj_scope + +let load_notation = + load_notation_common true let open_notation i (_, nobj) = let scope = nobj.notobj_scope in @@ -1331,7 +1341,7 @@ let open_notation i (_, nobj) = end let cache_notation o = - load_notation 1 o; + load_notation_common false 1 o; open_notation 1 o let subst_notation (subst, nobj) = @@ -1566,52 +1576,72 @@ let add_infix local env ({CAst.loc;v=inf},modifiers) pr sc = add_notation local env c (df,modifiers) sc (**********************************************************************) -(* Delimiters and classes bound to scopes *) +(* Scopes, delimiters and classes bound to scopes *) type scope_command = - | ScopeDelim of string + | ScopeDeclare + | ScopeDelimAdd of string + | ScopeDelimRemove | ScopeClasses of scope_class list - | ScopeRemove - -let load_scope_command _ (_,(scope,dlm)) = - Notation.declare_scope scope -let open_scope_command i (_,(scope,o)) = +let load_scope_command_common silently_define_scope_if_undefined _ (_,(local,scope,o)) = + let declare_scope_if_needed = + if silently_define_scope_if_undefined then Notation.declare_scope + else Notation.ensure_scope in + match o with + | ScopeDeclare -> Notation.declare_scope scope + (* When the default shall be to require that a scope already exists *) + (* the call to declare_scope_if_needed will have to be removed below *) + | ScopeDelimAdd dlm -> declare_scope_if_needed scope + | ScopeDelimRemove -> declare_scope_if_needed scope + | ScopeClasses cl -> declare_scope_if_needed scope + +let load_scope_command = + load_scope_command_common true + +let open_scope_command i (_,(local,scope,o)) = if Int.equal i 1 then match o with - | ScopeDelim dlm -> Notation.declare_delimiters scope dlm + | ScopeDeclare -> () + | ScopeDelimAdd dlm -> Notation.declare_delimiters scope dlm + | ScopeDelimRemove -> Notation.remove_delimiters scope | ScopeClasses cl -> List.iter (Notation.declare_scope_class scope) cl - | ScopeRemove -> Notation.remove_delimiters scope let cache_scope_command o = - load_scope_command 1 o; + load_scope_command_common false 1 o; open_scope_command 1 o -let subst_scope_command (subst,(scope,o as x)) = match o with +let subst_scope_command (subst,(local,scope,o as x)) = match o with | ScopeClasses cl -> let cl' = List.map_filter (subst_scope_class subst) cl in let cl' = if List.for_all2eq (==) cl cl' then cl else cl' in - scope, ScopeClasses cl' + local, scope, ScopeClasses cl' | _ -> x -let inScopeCommand : scope_name * scope_command -> obj = +let classify_scope_command (local, _, _ as o) = + if local then Dispose else Substitute o + +let inScopeCommand : locality_flag * scope_name * scope_command -> obj = declare_object {(default_object "DELIMITERS") with cache_function = cache_scope_command; open_function = open_scope_command; load_function = load_scope_command; subst_function = subst_scope_command; - classify_function = (fun obj -> Substitute obj)} + classify_function = classify_scope_command} + +let declare_scope local scope = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDeclare)) -let add_delimiters scope key = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeDelim key)) +let add_delimiters local scope key = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimAdd key)) -let remove_delimiters scope = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeRemove)) +let remove_delimiters local scope = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeDelimRemove)) -let add_class_scope scope cl = - Lib.add_anonymous_leaf (inScopeCommand(scope,ScopeClasses cl)) +let add_class_scope local scope cl = + Lib.add_anonymous_leaf (inScopeCommand(local,scope,ScopeClasses cl)) (* Check if abbreviation to a name and avoid early insertion of maximal implicit arguments *) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 73bee7121b..38dbdf7e41 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -27,11 +27,12 @@ val add_notation : locality_flag -> env -> constr_expr -> val add_notation_extra_printing_rule : string -> string -> string -> unit -(** Declaring delimiter keys and default scopes *) +(** Declaring scopes, delimiter keys and default scopes *) -val add_delimiters : scope_name -> string -> unit -val remove_delimiters : scope_name -> unit -val add_class_scope : scope_name -> scope_class list -> unit +val declare_scope : locality_flag -> scope_name -> unit +val add_delimiters : locality_flag -> scope_name -> string -> unit +val remove_delimiters : locality_flag -> scope_name -> unit +val add_class_scope : locality_flag -> scope_name -> scope_class list -> unit (** Add only the interpretation of a notation that already has pa/pp rules *) diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 93e4e89a12..63e9e4fe49 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -635,6 +635,10 @@ open Pputils keyword (if opening then "Open " else "Close ") ++ keyword "Scope" ++ spc() ++ str sc ) + | VernacDeclareScope sc -> + return ( + keyword "Declare Scope" ++ spc () ++ str sc + ) | VernacDelimiters (sc,Some key) -> return ( keyword "Delimit Scope" ++ spc () ++ str sc ++ diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e1c9712135..681dce3ca3 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -403,17 +403,24 @@ let dump_global r = (**********) (* Syntax *) -let vernac_syntax_extension atts infix l = +let vernac_syntax_extension ~atts infix l = let local = enforce_module_locality atts.locality in if infix then Metasyntax.check_infix_modifiers (snd l); Metasyntax.add_syntax_extension local l -let vernac_delimiters sc = function - | Some lr -> Metasyntax.add_delimiters sc lr - | None -> Metasyntax.remove_delimiters sc +let vernac_declare_scope ~atts sc = + let local = enforce_module_locality atts.locality in + Metasyntax.declare_scope local sc -let vernac_bind_scope sc cll = - Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll) +let vernac_delimiters ~atts sc action = + let local = enforce_module_locality atts.locality in + match action with + | Some lr -> Metasyntax.add_delimiters local sc lr + | None -> Metasyntax.remove_delimiters local sc + +let vernac_bind_scope ~atts sc cll = + let local = enforce_module_locality atts.locality in + Metasyntax.add_class_scope local sc (List.map scope_class_of_qualid cll) let vernac_open_close_scope ~atts (b,s) = let local = enforce_section_locality atts.locality in @@ -1692,36 +1699,37 @@ let query_command_selector ?loc = function let vernac_check_may_eval ~atts redexp glopt rc = let glopt = query_command_selector ?loc:atts.loc glopt in let (sigma, env) = get_current_context_of_args glopt in - let sigma', c = interp_open_constr env sigma rc in - let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in - Evarconv.check_problems_are_solved env sigma'; - let sigma' = Evd.minimize_universes sigma' in - let uctx = Evd.universe_context_set sigma' in - let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma' env) in + let sigma, c = interp_open_constr env sigma rc in + let sigma = Evarconv.solve_unif_constraints_with_heuristics env sigma in + Evarconv.check_problems_are_solved env sigma; + let sigma = Evd.minimize_universes sigma in + let uctx = Evd.universe_context_set sigma in + let env = Environ.push_context_set uctx (Evarutil.nf_env_evar sigma env) in let j = - if Evarutil.has_undefined_evars sigma' c then - Evarutil.j_nf_evar sigma' (Retyping.get_judgment_of env sigma' c) + if Evarutil.has_undefined_evars sigma c then + Evarutil.j_nf_evar sigma (Retyping.get_judgment_of env sigma c) else - let c = EConstr.to_constr sigma' c in + let c = EConstr.to_constr sigma c in (* OK to call kernel which does not support evars *) Termops.on_judgment EConstr.of_constr (Arguments_renaming.rename_typing env c) in - match redexp with + let pp = match redexp with | None -> - let evars_of_term c = Evarutil.undefined_evars_of_term sigma' c in + let evars_of_term c = Evarutil.undefined_evars_of_term sigma c in let l = Evar.Set.union (evars_of_term j.Environ.uj_val) (evars_of_term j.Environ.uj_type) in - let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma' j.Environ.uj_type } in - print_judgment env sigma' j ++ - pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ - Printer.pr_universe_ctx_set sigma uctx + let j = { j with Environ.uj_type = Reductionops.nf_betaiota env sigma j.Environ.uj_type } in + print_judgment env sigma j ++ + pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma l | Some r -> - let (sigma',r_interp) = Hook.get f_interp_redexp env sigma' r in + let (sigma,r_interp) = Hook.get f_interp_redexp env sigma r in let redfun env evm c = let (redfun, _) = reduction_of_red_expr env r_interp in let (_, c) = redfun env evm c in c in - print_eval redfun env sigma' rc j + print_eval redfun env sigma rc j + in + pp ++ Printer.pr_universe_ctx_set sigma uctx let vernac_declare_reduction ~atts s r = let local = make_locality atts.locality in @@ -1801,13 +1809,13 @@ let vernac_print ~atts env sigma = | PrintName (qid,udecl) -> dump_global qid; print_name env sigma qid udecl - | PrintGraph -> Prettyp.print_graph env sigma + | PrintGraph -> Prettyp.print_graph () | PrintClasses -> Prettyp.print_classes() | PrintTypeClasses -> Prettyp.print_typeclasses() | PrintInstances c -> Prettyp.print_instances (smart_global c) - | PrintCoercions -> Prettyp.print_coercions env sigma + | PrintCoercions -> Prettyp.print_coercions () | PrintCoercionPaths (cls,clt) -> - Prettyp.print_path_between env sigma (cl_of_qualid cls) (cl_of_qualid clt) + Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt) | PrintCanonicalConversions -> Prettyp.print_canonical_projections env sigma | PrintUniverses (b, dst) -> let univ = Global.universes () in @@ -2092,9 +2100,10 @@ let interp ?proof ~atts ~st c = (* Syntax *) | VernacSyntaxExtension (infix, sl) -> - vernac_syntax_extension atts infix sl - | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr - | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl + vernac_syntax_extension ~atts infix sl + | VernacDeclareScope sc -> vernac_declare_scope ~atts sc + | VernacDelimiters (sc,lr) -> vernac_delimiters ~atts sc lr + | VernacBindScope (sc,rl) -> vernac_bind_scope ~atts sc rl | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s) | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc | VernacNotation (c,infpl,sc) -> @@ -2231,6 +2240,7 @@ let check_vernac_supports_locality c l = | Some _, ( VernacOpenCloseScope _ | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _ + | VernacDeclareScope _ | VernacDelimiters _ | VernacBindScope _ | VernacDeclareCustomEntry _ | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _ | VernacAssumption _ | VernacStartTheoremProof _ diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 8fb74e6d78..11b2a7d802 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -325,6 +325,7 @@ type nonrec vernac_expr = (* Syntax *) | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) | VernacOpenCloseScope of bool * scope_name + | VernacDeclareScope of scope_name | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * class_rawexpr list | VernacInfix of (lstring * syntax_modifier list) * |