diff options
93 files changed, 805 insertions, 1083 deletions
diff --git a/clib/cString.ml b/clib/cString.ml index 111be3da82..423c08da13 100644 --- a/clib/cString.ml +++ b/clib/cString.ml @@ -17,16 +17,12 @@ sig val is_empty : string -> bool val explode : string -> string list val implode : string list -> string - val strip : string -> string - [@@ocaml.deprecated "Use [trim]"] val drop_simple_quotes : string -> string val string_index_from : string -> int -> string -> int val string_contains : where:string -> what:string -> bool val plural : int -> string -> string val conjugate_verb_to_be : int -> string val ordinal : int -> string - val split : char -> string -> string list - [@@ocaml.deprecated "Use [split_on_char]"] val is_sub : string -> string -> int -> bool module Set : Set.S with type elt = t module Map : CMap.ExtS with type key = t and module Set := Set @@ -59,8 +55,6 @@ let implode sl = String.concat "" sl let is_empty s = String.length s = 0 -let strip = String.trim - let drop_simple_quotes s = let n = String.length s in if n > 2 && s.[0] = '\'' && s.[n-1] = '\'' then String.sub s 1 (n-2) else s @@ -124,8 +118,6 @@ let ordinal n = (* string parsing *) -let split = String.split_on_char - module Self = struct type t = string diff --git a/clib/cString.mli b/clib/cString.mli index 364b6a34b1..f68bd3bb65 100644 --- a/clib/cString.mli +++ b/clib/cString.mli @@ -30,10 +30,6 @@ sig val implode : string list -> string (** [implode [s1; ...; sn]] returns [s1 ^ ... ^ sn] *) - val strip : string -> string - [@@ocaml.deprecated "Use [trim]"] - (** Alias for [String.trim] *) - val drop_simple_quotes : string -> string (** Remove the eventual first surrounding simple quotes of a string. *) @@ -52,10 +48,6 @@ sig val ordinal : int -> string (** Generate the ordinal number in English. *) - val split : char -> string -> string list - [@@ocaml.deprecated "Use [split_on_char]"] - (** [split c s] alias of [String.split_on_char] *) - val is_sub : string -> string -> int -> bool (** [is_sub p s off] tests whether [s] contains [p] at offset [off]. *) diff --git a/configure.ml b/configure.ml index 5b99851f83..57f31fec4c 100644 --- a/configure.ml +++ b/configure.ml @@ -17,6 +17,7 @@ let coq_macos_version = "8.9.90" (** "[...] should be a string comprised of three non-negative, period-separated integers [...]" *) let vo_magic = 8991 let state_magic = 58991 +let is_a_released_version = false let distributed_exec = ["coqtop.opt"; "coqidetop.opt"; "coqqueryworker.opt"; "coqproofworker.opt"; "coqtacticworker.opt"; "coqc.opt";"coqchk";"coqdoc";"coqworkmgr";"coq_makefile";"coq-tex";"coqwc";"csdpcert";"coqdep"] @@ -1205,8 +1206,8 @@ let write_configpy f = safe_remove f; let o = open_out f in let pr s = fprintf o s in - let pr_s = pr "%s = '%s'\n" in pr "# DO NOT EDIT THIS FILE: automatically generated by ../configure\n"; - pr_s "version" coq_version + pr "version = '%s'\n" coq_version; + pr "is_a_released_version = %s\n" (if is_a_released_version then "True" else "False") let _ = write_configpy "config/coq_config.py" diff --git a/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh new file mode 100644 index 0000000000..2015935dd9 --- /dev/null +++ b/dev/ci/user-overlays/10076-vbgl-canonical-disable-hint.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "10076" ] || [ "$CI_BRANCH" = "canonical-disable-hint" ]; then + + elpi_CI_REF=canonical-disable-hint + elpi_CI_GITURL=https://github.com/vbgl/coq-elpi + +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 9e0d47651e..7221c3de56 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,3 +1,10 @@ +## Changes between Coq 8.10 and Coq 8.11 + +### ML API + +- Functions and types deprecated in 8.10 have been removed in Coq + 8.11. + ## Changes between Coq 8.9 and Coq 8.10 ### ML4 Pre Processing diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md index 60c0886896..189d6f9fa5 100644 --- a/dev/doc/release-process.md +++ b/dev/doc/release-process.md @@ -84,10 +84,18 @@ Coq has been tagged. - [ ] Have some people test the recently auto-generated Windows and MacOS packages. -- [ ] Change the version name from alpha to beta1 (see +- [ ] In a PR: + - Change the version name from alpha to beta1 (see [#7009](https://github.com/coq/coq/pull/7009/files)). - We generally do not update the magic numbers at this point. + - We generally do not update the magic numbers at this point. + - Set `is_a_released_version` to `true` in `configure.ml`. - [ ] Put the `VX.X+beta1` tag using `git tag -s`. +- [ ] Check using `git push --tags --dry-run` that you are not + pushing anything else than the new tag. If needed, remove spurious + tags with `git tag -d`. When this is OK, proceed with `git push --tags`. +- [ ] Set `is_a_released_version` to `false` in `configure.ml` + (if you forget about it, you'll be reminded whenever you try to + backport a PR with a changelog entry). ### These steps are the same for all releases (beta, final, patch-level) ### @@ -112,9 +120,17 @@ ## At the final release time ## -- [ ] Change the version name to X.X.0 and the magic numbers (see +- [ ] In a PR: + - Change the version name from X.X.0 and the magic numbers (see [#7271](https://github.com/coq/coq/pull/7271/files)). + - Set `is_a_released_version` to `true` in `configure.ml`. - [ ] Put the `VX.X.0` tag. +- [ ] Check using `git push --tags --dry-run` that you are not + pushing anything else than the new tag. If needed, remove spurious + tags with `git tag -d`. When this is OK, proceed with `git push --tags`. +- [ ] Set `is_a_released_version` to `false` in `configure.ml` + (if you forget about it, you'll be reminded whenever you try to + backport a PR with a changelog entry). Repeat the generic process documented above for all releases. diff --git a/doc/changelog/02-specification-language/10076-not-canonical-projection.rst b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst new file mode 100644 index 0000000000..0a902079b9 --- /dev/null +++ b/doc/changelog/02-specification-language/10076-not-canonical-projection.rst @@ -0,0 +1,4 @@ +- Record fields can be annotated to prevent them from being used as canonical projections; + see :ref:`canonicalstructures` for details + (`#10076 <https://github.com/coq/coq/pull/10076>`_, + by Vincent Laporte). diff --git a/doc/changelog/04-tactics/09996-hint-mode.rst b/doc/changelog/04-tactics/09996-hint-mode.rst deleted file mode 100644 index 06e9059b45..0000000000 --- a/doc/changelog/04-tactics/09996-hint-mode.rst +++ /dev/null @@ -1,5 +0,0 @@ -- Modes are now taken into account by :tacn:`typeclasses eauto` for - local hypotheses - (`#9996 <https://github.com/coq/coq/pull/9996>`_, - fixes `#5752 <https://github.com/coq/coq/issues/5752>`_, - by Maxime Dénès, review by Pierre-Marie Pédrot). diff --git a/doc/changelog/04-tactics/10059-change-no-check.rst b/doc/changelog/04-tactics/10059-change-no-check.rst deleted file mode 100644 index 987b2a8ccd..0000000000 --- a/doc/changelog/04-tactics/10059-change-no-check.rst +++ /dev/null @@ -1,7 +0,0 @@ -- New variant :tacn:`change_no_check` of :tacn:`change`, usable as a - documented replacement of :tacn:`convert_concl_no_check` - (`#10012 <https://github.com/coq/coq/pull/10012>`_, - `#10017 <https://github.com/coq/coq/pull/10017>`_, - `#10053 <https://github.com/coq/coq/pull/10053>`_, and - `#10059 <https://github.com/coq/coq/pull/10059>`_, - by Hugo Herbelin and Paolo G. Giarrusso). diff --git a/doc/changelog/06-ssreflect/09995-notations.rst b/doc/changelog/06-ssreflect/09995-notations.rst deleted file mode 100644 index 3dfc45242d..0000000000 --- a/doc/changelog/06-ssreflect/09995-notations.rst +++ /dev/null @@ -1,8 +0,0 @@ -- `inE` now expands `y \in r x` when `r` is a `simpl_rel`. - New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion - class, simplified `predType` interface: `pred_class` and `mkPredType` - deprecated, `{pred T}` and `PredType` should be used instead. - `if c return t then ...` now expects `c` to be a variable bound in `t`. - New `nonPropType` interface matching types that do _not_ have sort `Prop`. - New `relpre R f` definition for the preimage of a relation R under f - (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier). diff --git a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst b/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst deleted file mode 100644 index 732c088f45..0000000000 --- a/doc/changelog/10-standard-library/09984-pairusualdecidabletypefull.rst +++ /dev/null @@ -1,3 +0,0 @@ -- Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull` - (`#9984 <https://github.com/coq/coq/pull/9984>`_, - by Jean-Christophe Léchenet and Oliver Nash). diff --git a/doc/changelog/12-misc/09964-changes.rst b/doc/changelog/12-misc/09964-changes.rst deleted file mode 100644 index 1113782180..0000000000 --- a/doc/changelog/12-misc/09964-changes.rst +++ /dev/null @@ -1,13 +0,0 @@ -- Changelog has been moved from a specific file `CHANGES.md` to the - reference manual; former Credits chapter of the reference manual has - been split in two parts: a History chapter which was enriched with - additional historical information about Coq versions 1 to 5, and a - Changes chapter which was enriched with the content formerly in - `CHANGES.md` and `COMPATIBILITY` - (`#9133 <https://github.com/coq/coq/pull/9133>`_, - `#9668 <https://github.com/coq/coq/pull/9668>`_, - `#9939 <https://github.com/coq/coq/pull/9939>`_, - `#9964 <https://github.com/coq/coq/pull/9964>`_, - by Théo Zimmermann, - with help and ideas from Emilio Jesús Gallego Arias, - Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi). diff --git a/doc/sphinx/addendum/canonical-structures.rst b/doc/sphinx/addendum/canonical-structures.rst index dd21ea09bd..b593b0cef1 100644 --- a/doc/sphinx/addendum/canonical-structures.rst +++ b/doc/sphinx/addendum/canonical-structures.rst @@ -209,7 +209,7 @@ We need to define a new class that inherits from both ``EQ`` and ``LE``. LE_class : LE.class T; extra : mixin (EQ.Pack T EQ_class) (LE.cmp T LE_class) }. - Structure type := _Pack { obj : Type; class_of : class obj }. + Structure type := _Pack { obj : Type; #[canonical(false)] class_of : class obj }. Arguments Mixin {e le} _. @@ -219,6 +219,9 @@ The mixin component of the ``LEQ`` class contains all the extra content we are adding to ``EQ`` and ``LE``. In particular it contains the requirement that the two relations we are combining are compatible. +The `class_of` projection of the `type` structure is annotated as *not canonical*; +it plays no role in the search for instances. + Unfortunately there is still an obstacle to developing the algebraic theory of this new class. @@ -313,9 +316,7 @@ constructor ``*``. It also tests that they work as expected. Unfortunately, these declarations are very verbose. In the following subsection we show how to make them more compact. -.. FIXME shouldn't warn - -.. coqtop:: all warn +.. coqtop:: all Module Add_instance_attempt. @@ -420,9 +421,7 @@ the reader can refer to :cite:`CSwcu`. The declaration of canonical instances can now be way more compact: -.. FIXME should not warn - -.. coqtop:: all warn +.. coqtop:: all Canonical Structure nat_LEQty := Eval hnf in Pack nat nat_LEQmx. diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 5704587ae0..cca3b2e06b 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -2,7 +2,9 @@ Recent changes -------------- -.. include:: ../unreleased.rst +.. ifconfig:: not coq_config.is_a_released_version + + .. include:: ../unreleased.rst Version 8.10 ------------ @@ -353,6 +355,11 @@ Other changes in 8.10+beta1 that will do it automatically, using the output of ``coqc`` (`#8638 <https://github.com/coq/coq/pull/8638>`_, by Jason Gross). + - Allow inspecting custom grammar entries by :cmd:`Print Custom Grammar` + (`#10061 <https://github.com/coq/coq/pull/10061>`_, + fixes `#9681 <http://github.com/coq/coq/pull/9681>`_, + by Jasper Hugunin, review by Pierre-Marie Pédrot and Hugo Herbelin). + - The `quote plugin <https://coq.inria.fr/distrib/V8.9.0/refman/proof-engine/detailed-tactic-examples.html#quote>`_ was removed. If some users are interested in maintaining this plugin @@ -398,7 +405,32 @@ Other changes in 8.10+beta1 closes `#7632 <https://github.com/coq/coq/issues/7632>`_, by Théo Zimmermann). - - SSReflect clear discipline made consistent across the entire proof language. + - Modes are now taken into account by :tacn:`typeclasses eauto` for + local hypotheses + (`#9996 <https://github.com/coq/coq/pull/9996>`_, + fixes `#5752 <https://github.com/coq/coq/issues/5752>`_, + by Maxime Dénès, review by Pierre-Marie Pédrot). + + - New variant :tacn:`change_no_check` of :tacn:`change`, usable as a + documented replacement of :tacn:`convert_concl_no_check` + (`#10012 <https://github.com/coq/coq/pull/10012>`_, + `#10017 <https://github.com/coq/coq/pull/10017>`_, + `#10053 <https://github.com/coq/coq/pull/10053>`_, and + `#10059 <https://github.com/coq/coq/pull/10059>`_, + by Hugo Herbelin and Paolo G. Giarrusso). + + - The simplified value returned by :tacn:`field_simplify` is not + always a fraction anymore. When the denominator is :g:`1`, it + returns :g:`x` while previously it was returning :g:`x/1`. This + change could break codes that were post-processing application of + :tacn:`field_simplify` to get rid of these :g:`x/1` + (`#9854 <https://github.com/coq/coq/pull/9854>`_, + by Laurent Théry, + with help from Michael Soegtrop, Maxime Dénès, and Vincent Laporte). + +- SSReflect: + + - Clear discipline made consistent across the entire proof language. Whenever a clear switch `{x..}` comes immediately before an existing proof context entry (used as a view, as a rewrite rule or as name for a new context entry) then such entry is cleared too. @@ -412,6 +444,15 @@ Other changes in 8.10+beta1 (`#9341 <https://github.com/coq/coq/pull/9341>`_, by Enrico Tassi). + - `inE` now expands `y \in r x` when `r` is a `simpl_rel`. + New `{pred T}` notation for a `pred T` alias in the `pred_sort` coercion + class, simplified `predType` interface: `pred_class` and `mkPredType` + deprecated, `{pred T}` and `PredType` should be used instead. + `if c return t then ...` now expects `c` to be a variable bound in `t`. + New `nonPropType` interface matching types that do _not_ have sort `Prop`. + New `relpre R f` definition for the preimage of a relation R under f + (`#9995 <https://github.com/coq/coq/pull/9995>`_, by Georges Gonthier). + - Vernacular commands: - Binders for an :cmd:`Instance` now act more like binders for a :cmd:`Theorem`. @@ -533,10 +574,28 @@ Other changes in 8.10+beta1 `fset` database (`#9725 <https://github.com/coq/coq/pull/9725>`_, by Frédéric Besson). + - Added :g:`Coq.Structures.EqualitiesFacts.PairUsualDecidableTypeFull` + (`#9984 <https://github.com/coq/coq/pull/9984>`_, + by Jean-Christophe Léchenet and Oliver Nash). + - Some error messages that show problems with a pair of non-matching values will now highlight the differences (`#8669 <https://github.com/coq/coq/pull/8669>`_, by Jim Fehrle). +- Changelog has been moved from a specific file `CHANGES.md` to the + reference manual; former Credits chapter of the reference manual has + been split in two parts: a History chapter which was enriched with + additional historical information about Coq versions 1 to 5, and a + Changes chapter which was enriched with the content formerly in + `CHANGES.md` and `COMPATIBILITY` + (`#9133 <https://github.com/coq/coq/pull/9133>`_, + `#9668 <https://github.com/coq/coq/pull/9668>`_, + `#9939 <https://github.com/coq/coq/pull/9939>`_, + `#9964 <https://github.com/coq/coq/pull/9964>`_, + and `#10085 <https://github.com/coq/coq/pull/10085>`_, + by Théo Zimmermann, + with help and ideas from Emilio Jesús Gallego Arias, Gaëtan + Gilbert, Clément Pit-Claudel, Matthieu Sozeau, and Enrico Tassi). Version 8.9 ----------- diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index 972a53ae36..ec3343dac6 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -53,6 +53,7 @@ needs_sphinx = '1.7.8' # extensions coming with Sphinx (named 'sphinx.ext.*') or your custom # ones. extensions = [ + 'sphinx.ext.ifconfig', 'sphinx.ext.mathjax', 'sphinx.ext.todo', 'sphinxcontrib.bibtex', @@ -100,6 +101,7 @@ def copy_formatspecific_files(app): def setup(app): app.connect('builder-inited', copy_formatspecific_files) + app.add_config_value('coq_config', coq_config, 'env') # The master toctree document. # We create this file in `copy_master_doc` above. diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 5308330820..ba766c8c3d 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -2048,6 +2048,21 @@ in :ref:`canonicalstructures`; here only a simple example is given. If a same field occurs in several canonical structures, then only the structure declared first as canonical is considered. + .. note:: + To prevent a field from being involved in the inference of canonical instances, + its declaration can be annotated with the :g:`#[canonical(false)]` attribute. + + .. example:: + + For instance, when declaring the :g:`Setoid` structure above, the + :g:`Prf_equiv` field declaration could be written as follows. + + .. coqdoc:: + + #[canonical(false)] Prf_equiv : equivalence Carrier Equal + + See :ref:`canonicalstructures` for a more realistic example. + .. cmdv:: Canonical {? Structure } @ident {? : @type } := @term This is equivalent to a regular definition of :token:`ident` followed by the @@ -2067,6 +2082,10 @@ in :ref:`canonicalstructures`; here only a simple example is given. Print Canonical Projections. + .. note:: + + The last line would not show up if the corresponding projection (namely + :g:`Prf_equiv`) were annotated as not canonical, as described above. Implicit types of variables ~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 6cbd00f45d..efb5df720a 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -181,7 +181,14 @@ presented as a notebook. The first section is for selecting the text font used for scripts, goal and message windows. -The second section is devoted to file management: you may configure +The second and third sections are for controlling colors and style. + +The fourth section is for customizing the editor. It includes in +particular the ability to activate an Emacs mode named +micro-Proof-General (use the Help menu to know more about the +available bindings). + +The next section is devoted to file management: you may configure automatic saving of files, by periodically saving the contents into files named `#f#` for each opened file `f`. You may also activate the *revert* feature: in case a opened file is modified on the disk by a diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index b629d15b11..0ace9ef5b9 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -396,381 +396,3 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: none Qed. - -Using the tactic language -------------------------- - - -About the cardinality of the set of natural numbers -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -The first example which shows how to use pattern matching over the -proof context is a proof of the fact that natural numbers have more -than two elements. This can be done as follows: - -.. coqtop:: in reset - - Lemma card_nat : - ~ exists x : nat, exists y : nat, forall z:nat, x = z \/ y = z. - Proof. - -.. coqtop:: in - - red; intros (x, (y, Hy)). - -.. coqtop:: in - - elim (Hy 0); elim (Hy 1); elim (Hy 2); intros; - - match goal with - | _ : ?a = ?b, _ : ?a = ?c |- _ => - cut (b = c); [ discriminate | transitivity a; auto ] - end. - -.. coqtop:: in - - Qed. - -We can notice that all the (very similar) cases coming from the three -eliminations (with three distinct natural numbers) are successfully -solved by a match goal structure and, in particular, with only one -pattern (use of non-linear matching). - - -Permutations of lists -~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -A more complex example is the problem of permutations of -lists. The aim is to show that a list is a permutation of -another list. - -.. coqtop:: in reset - - Section Sort. - -.. coqtop:: in - - Variable A : Set. - -.. coqtop:: in - - Inductive perm : list A -> list A -> Prop := - | perm_refl : forall l, perm l l - | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1) - | perm_append : forall a l, perm (a :: l) (l ++ a :: nil) - | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2. - -.. coqtop:: in - - End Sort. - -First, we define the permutation predicate as shown above. - -.. coqtop:: none - - Require Import List. - - -.. coqtop:: in - - Ltac perm_aux n := - match goal with - | |- (perm _ ?l ?l) => apply perm_refl - | |- (perm _ (?a :: ?l1) (?a :: ?l2)) => - let newn := eval compute in (length l1) in - (apply perm_cons; perm_aux newn) - | |- (perm ?A (?a :: ?l1) ?l2) => - match eval compute in n with - | 1 => fail - | _ => - let l1' := constr:(l1 ++ a :: nil) in - (apply (perm_trans A (a :: l1) l1' l2); - [ apply perm_append | compute; perm_aux (pred n) ]) - end - end. - -Next we define an auxiliary tactic ``perm_aux`` which takes an argument -used to control the recursion depth. This tactic behaves as follows. If -the lists are identical (i.e. convertible), it concludes. Otherwise, if -the lists have identical heads, it proceeds to look at their tails. -Finally, if the lists have different heads, it rotates the first list by -putting its head at the end if the new head hasn't been the head previously. To check this, we keep track of the -number of performed rotations using the argument ``n``. We do this by -decrementing ``n`` each time we perform a rotation. It works because -for a list of length ``n`` we can make exactly ``n - 1`` rotations -to generate at most ``n`` distinct lists. Notice that we use the natural -numbers of Coq for the rotation counter. From :ref:`ltac-syntax` we know -that it is possible to use the usual natural numbers, but they are only -used as arguments for primitive tactics and they cannot be handled, so, -in particular, we cannot make computations with them. Thus the natural -choice is to use Coq data structures so that Coq makes the computations -(reductions) by ``eval compute in`` and we can get the terms back by match. - -.. coqtop:: in - - Ltac solve_perm := - match goal with - | |- (perm _ ?l1 ?l2) => - match eval compute in (length l1 = length l2) with - | (?n = ?n) => perm_aux n - end - end. - -The main tactic is ``solve_perm``. It computes the lengths of the two lists -and uses them as arguments to call ``perm_aux`` if the lengths are equal (if they -aren't, the lists cannot be permutations of each other). Using this tactic we -can now prove lemmas as follows: - -.. coqtop:: in - - Lemma solve_perm_ex1 : - perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). - Proof. solve_perm. Qed. - -.. coqtop:: in - - Lemma solve_perm_ex2 : - perm nat - (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) - (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). - Proof. solve_perm. Qed. - -Deciding intuitionistic propositional logic -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - -Pattern matching on goals allows a powerful backtracking when returning tactic -values. An interesting application is the problem of deciding intuitionistic -propositional logic. Considering the contraction-free sequent calculi LJT* of -Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the -tactic language as shown below. - -.. coqtop:: in reset - - Ltac basic := - match goal with - | |- True => trivial - | _ : False |- _ => contradiction - | _ : ?A |- ?A => assumption - end. - -.. coqtop:: in - - Ltac simplify := - repeat (intros; - match goal with - | H : ~ _ |- _ => red in H - | H : _ /\ _ |- _ => - elim H; do 2 intro; clear H - | H : _ \/ _ |- _ => - elim H; intro; clear H - | H : ?A /\ ?B -> ?C |- _ => - cut (A -> B -> C); - [ intro | intros; apply H; split; assumption ] - | H: ?A \/ ?B -> ?C |- _ => - cut (B -> C); - [ cut (A -> C); - [ intros; clear H - | intro; apply H; left; assumption ] - | intro; apply H; right; assumption ] - | H0 : ?A -> ?B, H1 : ?A |- _ => - cut B; [ intro; clear H0 | apply H0; assumption ] - | |- _ /\ _ => split - | |- ~ _ => red - end). - -.. coqtop:: in - - Ltac my_tauto := - simplify; basic || - match goal with - | H : (?A -> ?B) -> ?C |- _ => - cut (B -> C); - [ intro; cut (A -> B); - [ intro; cut C; - [ intro; clear H | apply H; assumption ] - | clear H ] - | intro; apply H; intro; assumption ]; my_tauto - | H : ~ ?A -> ?B |- _ => - cut (False -> B); - [ intro; cut (A -> False); - [ intro; cut B; - [ intro; clear H | apply H; assumption ] - | clear H ] - | intro; apply H; red; intro; assumption ]; my_tauto - | |- _ \/ _ => (left; my_tauto) || (right; my_tauto) - end. - -The tactic ``basic`` tries to reason using simple rules involving truth, falsity -and available assumptions. The tactic ``simplify`` applies all the reversible -rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main -tactic to be called) simplifies with ``simplify``, tries to conclude with -``basic`` and tries several paths using the backtracking rules (one of the -four Dyckhoff’s rules for the left implication to get rid of the contraction -and the right ``or``). - -Having defined ``my_tauto``, we can prove tautologies like these: - -.. coqtop:: in - - Lemma my_tauto_ex1 : - forall A B : Prop, A /\ B -> A \/ B. - Proof. my_tauto. Qed. - -.. coqtop:: in - - Lemma my_tauto_ex2 : - forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. - Proof. my_tauto. Qed. - - -Deciding type isomorphisms -~~~~~~~~~~~~~~~~~~~~~~~~~~ - -A more tricky problem is to decide equalities between types modulo -isomorphisms. Here, we choose to use the isomorphisms of the simply -typed λ-calculus with Cartesian product and unit type (see, for -example, :cite:`RC95`). The axioms of this λ-calculus are given below. - -.. coqtop:: in reset - - Open Scope type_scope. - -.. coqtop:: in - - Section Iso_axioms. - -.. coqtop:: in - - Variables A B C : Set. - -.. coqtop:: in - - Axiom Com : A * B = B * A. - - Axiom Ass : A * (B * C) = A * B * C. - - Axiom Cur : (A * B -> C) = (A -> B -> C). - - Axiom Dis : (A -> B * C) = (A -> B) * (A -> C). - - Axiom P_unit : A * unit = A. - - Axiom AR_unit : (A -> unit) = unit. - - Axiom AL_unit : (unit -> A) = A. - -.. coqtop:: in - - Lemma Cons : B = C -> A * B = A * C. - - Proof. - - intro Heq; rewrite Heq; reflexivity. - - Qed. - -.. coqtop:: in - - End Iso_axioms. - -.. coqtop:: in - - Ltac simplify_type ty := - match ty with - | ?A * ?B * ?C => - rewrite <- (Ass A B C); try simplify_type_eq - | ?A * ?B -> ?C => - rewrite (Cur A B C); try simplify_type_eq - | ?A -> ?B * ?C => - rewrite (Dis A B C); try simplify_type_eq - | ?A * unit => - rewrite (P_unit A); try simplify_type_eq - | unit * ?B => - rewrite (Com unit B); try simplify_type_eq - | ?A -> unit => - rewrite (AR_unit A); try simplify_type_eq - | unit -> ?B => - rewrite (AL_unit B); try simplify_type_eq - | ?A * ?B => - (simplify_type A; try simplify_type_eq) || - (simplify_type B; try simplify_type_eq) - | ?A -> ?B => - (simplify_type A; try simplify_type_eq) || - (simplify_type B; try simplify_type_eq) - end - with simplify_type_eq := - match goal with - | |- ?A = ?B => try simplify_type A; try simplify_type B - end. - -.. coqtop:: in - - Ltac len trm := - match trm with - | _ * ?B => let succ := len B in constr:(S succ) - | _ => constr:(1) - end. - -.. coqtop:: in - - Ltac assoc := repeat rewrite <- Ass. - -.. coqtop:: in - - Ltac solve_type_eq n := - match goal with - | |- ?A = ?A => reflexivity - | |- ?A * ?B = ?A * ?C => - apply Cons; let newn := len B in solve_type_eq newn - | |- ?A * ?B = ?C => - match eval compute in n with - | 1 => fail - | _ => - pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n) - end - end. - -.. coqtop:: in - - Ltac compare_structure := - match goal with - | |- ?A = ?B => - let l1 := len A - with l2 := len B in - match eval compute in (l1 = l2) with - | ?n = ?n => solve_type_eq n - end - end. - -.. coqtop:: in - - Ltac solve_iso := simplify_type_eq; compare_structure. - -The tactic to judge equalities modulo this axiomatization is shown above. -The algorithm is quite simple. First types are simplified using axioms that -can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``). -The normal forms are sequences of Cartesian products without Cartesian product -in the left component. These normal forms are then compared modulo permutation -of the components by the tactic ``compare_structure``. If they have the same -lengths, the tactic ``solve_type_eq`` attempts to prove that the types are equal. -The main tactic that puts all these components together is called ``solve_iso``. - -Here are examples of what can be solved by ``solve_iso``. - -.. coqtop:: in - - Lemma solve_iso_ex1 : - forall A B : Set, A * unit * B = B * (unit * A). - Proof. - intros; solve_iso. - Qed. - -.. coqtop:: in - - Lemma solve_iso_ex2 : - forall A B C : Set, - (A * unit -> B * (C * unit)) = - (A * unit -> (C -> unit) * C) * (unit -> A -> B). - Proof. - intros; solve_iso. - Qed. diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index d3562b52c5..a7eb7c2319 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -3,12 +3,25 @@ Ltac ==== -This chapter gives a compact documentation of |Ltac|, the tactic language -available in |Coq|. We start by giving the syntax, and next, we present the -informal semantics. If you want to know more regarding this language and -especially about its foundations, you can refer to :cite:`Del00`. Chapter -:ref:`detailedexamplesoftactics` is devoted to giving small but nontrivial -use examples of this language. +This chapter documents the tactic language |Ltac|. + +We start by giving the syntax, and next, we present the informal +semantics. To learn more about the language and +especially about its foundations, please refer to :cite:`Del00`. + +.. example:: Basic tactic macros + + Here are some examples of simple tactic macros that the + language lets you write. + + .. coqdoc:: + + Ltac reduce_and_try_to_solve := simpl; intros; auto. + + Ltac destruct_bool_and_rewrite b H1 H2 := + destruct b; [ rewrite H1; eauto | rewrite H2; eauto ]. + + See Section :ref:`ltac-examples` for more advanced examples. .. _ltac-syntax: @@ -1160,6 +1173,399 @@ Printing |Ltac| tactics This command displays a list of all user-defined tactics, with their arguments. + +.. _ltac-examples: + +Examples of using |Ltac| +------------------------- + +Proof that the natural numbers have at least two elements +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. example:: Proof that the natural numbers have at least two elements + + The first example shows how to use pattern matching over the proof + context to prove that natural numbers have at least two + elements. This can be done as follows: + + .. coqtop:: reset all + + Lemma card_nat : + ~ exists x y : nat, forall z:nat, x = z \/ y = z. + Proof. + intros (x & y & Hz). + destruct (Hz 0), (Hz 1), (Hz 2). + + At this point, the :tacn:`congruence` tactic would finish the job: + + .. coqtop:: all abort + + all: congruence. + + But for the purpose of the example, let's craft our own custom + tactic to solve this: + + .. coqtop:: none + + Lemma card_nat : + ~ exists x y : nat, forall z:nat, x = z \/ y = z. + Proof. + intros (x & y & Hz). + destruct (Hz 0), (Hz 1), (Hz 2). + + .. coqtop:: all abort + + all: match goal with + | _ : ?a = ?b, _ : ?a = ?c |- _ => assert (b = c) by now transitivity a + end. + all: discriminate. + + Notice that all the (very similar) cases coming from the three + eliminations (with three distinct natural numbers) are successfully + solved by a ``match goal`` structure and, in particular, with only one + pattern (use of non-linear matching). + + +Proving that a list is a permutation of a second list +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +.. example:: Proving that a list is a permutation of a second list + + Let's first define the permutation predicate: + + .. coqtop:: in reset + + Section Sort. + + Variable A : Set. + + Inductive perm : list A -> list A -> Prop := + | perm_refl : forall l, perm l l + | perm_cons : forall a l0 l1, perm l0 l1 -> perm (a :: l0) (a :: l1) + | perm_append : forall a l, perm (a :: l) (l ++ a :: nil) + | perm_trans : forall l0 l1 l2, perm l0 l1 -> perm l1 l2 -> perm l0 l2. + + End Sort. + + .. coqtop:: none + + Require Import List. + + + Next we define an auxiliary tactic :g:`perm_aux` which takes an + argument used to control the recursion depth. This tactic works as + follows: If the lists are identical (i.e. convertible), it + completes the proof. Otherwise, if the lists have identical heads, + it looks at their tails. Finally, if the lists have different + heads, it rotates the first list by putting its head at the end. + + Every time we perform a rotation, we decrement :g:`n`. When :g:`n` + drops down to :g:`1`, we stop performing rotations and we fail. + The idea is to give the length of the list as the initial value of + :g:`n`. This way of counting the number of rotations will avoid + going back to a head that had been considered before. + + From Section :ref:`ltac-syntax` we know that Ltac has a primitive + notion of integers, but they are only used as arguments for + primitive tactics and we cannot make computations with them. Thus, + instead, we use Coq's natural number type :g:`nat`. + + .. coqtop:: in + + Ltac perm_aux n := + match goal with + | |- (perm _ ?l ?l) => apply perm_refl + | |- (perm _ (?a :: ?l1) (?a :: ?l2)) => + let newn := eval compute in (length l1) in + (apply perm_cons; perm_aux newn) + | |- (perm ?A (?a :: ?l1) ?l2) => + match eval compute in n with + | 1 => fail + | _ => + let l1' := constr:(l1 ++ a :: nil) in + (apply (perm_trans A (a :: l1) l1' l2); + [ apply perm_append | compute; perm_aux (pred n) ]) + end + end. + + + The main tactic is :g:`solve_perm`. It computes the lengths of the + two lists and uses them as arguments to call :g:`perm_aux` if the + lengths are equal. (If they aren't, the lists cannot be + permutations of each other.) + + .. coqtop:: in + + Ltac solve_perm := + match goal with + | |- (perm _ ?l1 ?l2) => + match eval compute in (length l1 = length l2) with + | (?n = ?n) => perm_aux n + end + end. + + And now, here is how we can use the tactic :g:`solve_perm`: + + .. coqtop:: out + + Goal perm nat (1 :: 2 :: 3 :: nil) (3 :: 2 :: 1 :: nil). + + .. coqtop:: all abort + + solve_perm. + + .. coqtop:: out + + Goal perm nat + (0 :: 1 :: 2 :: 3 :: 4 :: 5 :: 6 :: 7 :: 8 :: 9 :: nil) + (0 :: 2 :: 4 :: 6 :: 8 :: 9 :: 7 :: 5 :: 3 :: 1 :: nil). + + .. coqtop:: all abort + + solve_perm. + + +Deciding intuitionistic propositional logic +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +Pattern matching on goals allows powerful backtracking when returning tactic +values. An interesting application is the problem of deciding intuitionistic +propositional logic. Considering the contraction-free sequent calculi LJT* of +Roy Dyckhoff :cite:`Dyc92`, it is quite natural to code such a tactic using the +tactic language as shown below. + +.. coqtop:: in reset + + Ltac basic := + match goal with + | |- True => trivial + | _ : False |- _ => contradiction + | _ : ?A |- ?A => assumption + end. + +.. coqtop:: in + + Ltac simplify := + repeat (intros; + match goal with + | H : ~ _ |- _ => red in H + | H : _ /\ _ |- _ => + elim H; do 2 intro; clear H + | H : _ \/ _ |- _ => + elim H; intro; clear H + | H : ?A /\ ?B -> ?C |- _ => + cut (A -> B -> C); + [ intro | intros; apply H; split; assumption ] + | H: ?A \/ ?B -> ?C |- _ => + cut (B -> C); + [ cut (A -> C); + [ intros; clear H + | intro; apply H; left; assumption ] + | intro; apply H; right; assumption ] + | H0 : ?A -> ?B, H1 : ?A |- _ => + cut B; [ intro; clear H0 | apply H0; assumption ] + | |- _ /\ _ => split + | |- ~ _ => red + end). + +.. coqtop:: in + + Ltac my_tauto := + simplify; basic || + match goal with + | H : (?A -> ?B) -> ?C |- _ => + cut (B -> C); + [ intro; cut (A -> B); + [ intro; cut C; + [ intro; clear H | apply H; assumption ] + | clear H ] + | intro; apply H; intro; assumption ]; my_tauto + | H : ~ ?A -> ?B |- _ => + cut (False -> B); + [ intro; cut (A -> False); + [ intro; cut B; + [ intro; clear H | apply H; assumption ] + | clear H ] + | intro; apply H; red; intro; assumption ]; my_tauto + | |- _ \/ _ => (left; my_tauto) || (right; my_tauto) + end. + +The tactic ``basic`` tries to reason using simple rules involving truth, falsity +and available assumptions. The tactic ``simplify`` applies all the reversible +rules of Dyckhoff’s system. Finally, the tactic ``my_tauto`` (the main +tactic to be called) simplifies with ``simplify``, tries to conclude with +``basic`` and tries several paths using the backtracking rules (one of the +four Dyckhoff’s rules for the left implication to get rid of the contraction +and the right ``or``). + +Having defined ``my_tauto``, we can prove tautologies like these: + +.. coqtop:: in + + Lemma my_tauto_ex1 : + forall A B : Prop, A /\ B -> A \/ B. + Proof. my_tauto. Qed. + +.. coqtop:: in + + Lemma my_tauto_ex2 : + forall A B : Prop, (~ ~ B -> B) -> (A -> B) -> ~ ~ A -> B. + Proof. my_tauto. Qed. + + +Deciding type isomorphisms +~~~~~~~~~~~~~~~~~~~~~~~~~~ + +A trickier problem is to decide equalities between types modulo +isomorphisms. Here, we choose to use the isomorphisms of the simply +typed λ-calculus with Cartesian product and unit type (see, for +example, :cite:`RC95`). The axioms of this λ-calculus are given below. + +.. coqtop:: in reset + + Open Scope type_scope. + +.. coqtop:: in + + Section Iso_axioms. + +.. coqtop:: in + + Variables A B C : Set. + +.. coqtop:: in + + Axiom Com : A * B = B * A. + + Axiom Ass : A * (B * C) = A * B * C. + + Axiom Cur : (A * B -> C) = (A -> B -> C). + + Axiom Dis : (A -> B * C) = (A -> B) * (A -> C). + + Axiom P_unit : A * unit = A. + + Axiom AR_unit : (A -> unit) = unit. + + Axiom AL_unit : (unit -> A) = A. + +.. coqtop:: in + + Lemma Cons : B = C -> A * B = A * C. + + Proof. + + intro Heq; rewrite Heq; reflexivity. + + Qed. + +.. coqtop:: in + + End Iso_axioms. + +.. coqtop:: in + + Ltac simplify_type ty := + match ty with + | ?A * ?B * ?C => + rewrite <- (Ass A B C); try simplify_type_eq + | ?A * ?B -> ?C => + rewrite (Cur A B C); try simplify_type_eq + | ?A -> ?B * ?C => + rewrite (Dis A B C); try simplify_type_eq + | ?A * unit => + rewrite (P_unit A); try simplify_type_eq + | unit * ?B => + rewrite (Com unit B); try simplify_type_eq + | ?A -> unit => + rewrite (AR_unit A); try simplify_type_eq + | unit -> ?B => + rewrite (AL_unit B); try simplify_type_eq + | ?A * ?B => + (simplify_type A; try simplify_type_eq) || + (simplify_type B; try simplify_type_eq) + | ?A -> ?B => + (simplify_type A; try simplify_type_eq) || + (simplify_type B; try simplify_type_eq) + end + with simplify_type_eq := + match goal with + | |- ?A = ?B => try simplify_type A; try simplify_type B + end. + +.. coqtop:: in + + Ltac len trm := + match trm with + | _ * ?B => let succ := len B in constr:(S succ) + | _ => constr:(1) + end. + +.. coqtop:: in + + Ltac assoc := repeat rewrite <- Ass. + +.. coqtop:: in + + Ltac solve_type_eq n := + match goal with + | |- ?A = ?A => reflexivity + | |- ?A * ?B = ?A * ?C => + apply Cons; let newn := len B in solve_type_eq newn + | |- ?A * ?B = ?C => + match eval compute in n with + | 1 => fail + | _ => + pattern (A * B) at 1; rewrite Com; assoc; solve_type_eq (pred n) + end + end. + +.. coqtop:: in + + Ltac compare_structure := + match goal with + | |- ?A = ?B => + let l1 := len A + with l2 := len B in + match eval compute in (l1 = l2) with + | ?n = ?n => solve_type_eq n + end + end. + +.. coqtop:: in + + Ltac solve_iso := simplify_type_eq; compare_structure. + +The tactic to judge equalities modulo this axiomatization is shown above. +The algorithm is quite simple. First types are simplified using axioms that +can be oriented (this is done by ``simplify_type`` and ``simplify_type_eq``). +The normal forms are sequences of Cartesian products without a Cartesian product +in the left component. These normal forms are then compared modulo permutation +of the components by the tactic ``compare_structure``. If they have the same +length, the tactic ``solve_type_eq`` attempts to prove that the types are equal. +The main tactic that puts all these components together is ``solve_iso``. + +Here are examples of what can be solved by ``solve_iso``. + +.. coqtop:: in + + Lemma solve_iso_ex1 : + forall A B : Set, A * unit * B = B * (unit * A). + Proof. + intros; solve_iso. + Qed. + +.. coqtop:: in + + Lemma solve_iso_ex2 : + forall A B C : Set, + (A * unit -> B * (C * unit)) = + (A * unit -> (C -> unit) * C) * (unit -> A -> B). + Proof. + intros; solve_iso. + Qed. + + Debugging |Ltac| tactics ------------------------ diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 0f78a9b84a..c728b925ac 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3561,7 +3561,7 @@ Automation .. tacn:: autorewrite with {+ @ident} :name: autorewrite - This tactic [4]_ carries out rewritings according to the rewriting rule + This tactic carries out rewritings according to the rewriting rule bases :n:`{+ @ident}`. Each rewriting rule from the base :n:`@ident` is applied to the main subgoal until @@ -4661,9 +4661,12 @@ Non-logical tactics .. example:: - .. coqtop:: all reset + .. coqtop:: none reset Parameter P : nat -> Prop. + + .. coqtop:: all abort + Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. all: cycle 2. @@ -4679,9 +4682,8 @@ Non-logical tactics .. example:: - .. coqtop:: reset all + .. coqtop:: all abort - Parameter P : nat -> Prop. Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. all: swap 1 3. @@ -4694,9 +4696,8 @@ Non-logical tactics .. example:: - .. coqtop:: all reset + .. coqtop:: all abort - Parameter P : nat -> Prop. Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. repeat split. all: revgoals. @@ -4717,7 +4718,7 @@ Non-logical tactics .. example:: - .. coqtop:: all reset + .. coqtop:: all abort Goal exists n, n=0. refine (ex_intro _ _ _). @@ -4746,39 +4747,6 @@ Non-logical tactics The ``give_up`` tactic can be used while editing a proof, to choose to write the proof script in a non-sequential order. -Simple tactic macros -------------------------- - -A simple example has more value than a long explanation: - -.. example:: - - .. coqtop:: reset all - - Ltac Solve := simpl; intros; auto. - - Ltac ElimBoolRewrite b H1 H2 := - elim b; [ intros; rewrite H1; eauto | intros; rewrite H2; eauto ]. - -The tactics macros are synchronous with the Coq section mechanism: a -tactic definition is deleted from the current environment when you -close the section (see also :ref:`section-mechanism`) where it was -defined. If you want that a tactic macro defined in a module is usable in the -modules that require it, you should put it outside of any section. - -:ref:`ltac` gives examples of more complex -user-defined tactics. - -.. [1] Actually, only the second subgoal will be generated since the - other one can be automatically checked. -.. [2] This corresponds to the cut rule of sequent calculus. -.. [3] Reminder: opaque constants will not be expanded by δ reductions. -.. [4] The behavior of this tactic has changed a lot compared to the - versions available in the previous distributions (V6). This may cause - significant changes in your theories to obtain the same result. As a - drawback of the re-engineering of the code, this tactic has also been - completely revised to get a very compact and readable version. - Delaying solving unification constraints ---------------------------------------- @@ -4917,3 +4885,8 @@ Performance-oriented tactic variants Goal False. native_cast_no_check I. Fail Qed. + +.. [1] Actually, only the second subgoal will be generated since the + other one can be automatically checked. +.. [2] This corresponds to the cut rule of sequent calculus. +.. [3] Reminder: opaque constants will not be expanded by δ reductions. diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index ac079ea7d5..edec13f681 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -840,10 +840,11 @@ gives a way to let any arbitrary expression which is not handled by the custom entry ``expr`` be parsed or printed by the main grammar of term up to the insertion of a pair of curly brackets. -.. cmd:: Print Grammar @ident. +.. cmd:: Print Custom Grammar @ident. + :name: Print Custom Grammar - This displays the state of the grammar for terms and grammar for - patterns associated to the custom entry :token:`ident`. + This displays the state of the grammar for terms associated to + the custom entry :token:`ident`. Summary ~~~~~~~ diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 96beb72a56..be0318fbde 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -26,24 +26,7 @@ let safe_evar_value sigma ev = try Some (EConstr.Unsafe.to_constr @@ Evd.existential_value sigma ev) with NotInstantiatedEvar | Not_found -> None -(** Combinators *) - -let evd_comb0 f evdref = - let (evd',x) = f !evdref in - evdref := evd'; - x - -let evd_comb1 f evdref x = - let (evd',y) = f !evdref x in - evdref := evd'; - y - -let evd_comb2 f evdref x y = - let (evd',z) = f !evdref x y in - evdref := evd'; - z - -let new_global evd x = +let new_global evd x = let (evd, c) = Evd.fresh_global (Global.env()) evd x in (evd, c) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index bb0da44103..8eaff8bd13 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -274,15 +274,6 @@ val push_rel_context_to_named_context : ?hypnaming:naming_mode -> val generalize_evar_over_rels : evar_map -> existential -> types * constr list -(** Evar combinators *) - -val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a -[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"] -val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a -[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"] -val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a -[@@ocaml.deprecated "References to [evar_map] are deprecated, please update your API calls"] - val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located -> Evar_kinds.t Loc.located diff --git a/engine/evd.ml b/engine/evd.ml index b89222cf8e..d37b49e2dc 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -869,8 +869,6 @@ let to_universe_context evd = UState.context evd.universes let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes -let const_univ_entry = univ_entry - let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl let restrict_universe_context evd vars = diff --git a/engine/evd.mli b/engine/evd.mli index b0fcddb068..29235050b0 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -615,9 +615,6 @@ val to_universe_context : evar_map -> Univ.UContext.t val univ_entry : poly:bool -> evar_map -> Entries.universes_entry -val const_univ_entry : poly:bool -> evar_map -> Entries.universes_entry -[@@ocaml.deprecated "Use [univ_entry]."] - val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.universes_entry val merge_universe_context : evar_map -> UState.t -> evar_map diff --git a/engine/ftactic.ml b/engine/ftactic.ml index ac0344148a..dab2e7d5ef 100644 --- a/engine/ftactic.ml +++ b/engine/ftactic.ml @@ -56,13 +56,6 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l) -let nf_enter f = - bind goals - (fun gl -> - gl >>= fun gl -> - Proofview.Goal.normalize gl >>= fun nfgl -> - Proofview.V82.wrap_exceptions (fun () -> f nfgl)) [@warning "-3"] - let enter f = bind goals (fun gl -> gl >>= fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl)) diff --git a/engine/ftactic.mli b/engine/ftactic.mli index 3c4fa6f4e8..ed95d62bc6 100644 --- a/engine/ftactic.mli +++ b/engine/ftactic.mli @@ -41,9 +41,6 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic (** {5 Focussing} *) -val nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t -[@@ocaml.deprecated "Normalization is enforced by EConstr, please use [enter]"] - (** Enter a goal. The resulting tactic is focussed. *) val enter : (Proofview.Goal.t -> 'a t) -> 'a t diff --git a/engine/proofview.ml b/engine/proofview.ml index f278c83912..ecea637947 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1104,13 +1104,6 @@ module Goal = struct tclZERO ~info e end end - - let normalize { self; state } = - Env.get >>= fun env -> - tclEVARMAP >>= fun sigma -> - let (gl,sigma) = nf_gmake env sigma (goal_with_state self state) in - tclTHEN (Unsafe.tclEVARS sigma) (tclUNIT gl) - let gmake env sigma goal = let state = get_state goal in let goal = drop_state goal in diff --git a/engine/proofview.mli b/engine/proofview.mli index 9455dae643..92f8b86df5 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -505,10 +505,6 @@ module Goal : sig (** Type of goals. *) type t - (** Normalises the argument goal. *) - val normalize : t -> t tactic - [@@ocaml.deprecated "Normalization is enforced by EConstr, [normalize] is not needed anymore"] - (** [concl], [hyps], [env] and [sigma] given a goal [gl] return respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the diff --git a/engine/termops.ml b/engine/termops.ml index 8e12c9be88..8a6bd17948 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -25,11 +25,6 @@ module CompactedDecl = Context.Compacted.Declaration module Internal = struct -let pr_sort_family = Sorts.pr_sort_family -[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"] -let pr_fix = Constr.debug_print_fix -[@@ocaml.deprecated "Use [Constr.debug_print_fix]"] - let debug_print_constr c = Constr.debug_print EConstr.Unsafe.(to_constr c) let debug_print_constr_env env sigma c = Constr.debug_print EConstr.(to_constr sigma c) let term_printer = ref debug_print_constr_env @@ -761,13 +756,6 @@ let fold_constr_with_binders sigma g f n acc c = let c = Unsafe.to_constr (whd_evar sigma c) in Constr.fold_constr_with_binders g f n acc c -(* [iter_constr_with_full_binders g f acc c] iters [f acc] on the immediate - subterms of [c]; it carries an extra data [acc] which is processed by [g] at - each binder traversal; it is not recursive and the order with which - subterms are processed is not specified *) - -let iter_constr_with_full_binders = EConstr.iter_with_full_binders - (***************************) (* occurs check functions *) (***************************) @@ -862,8 +850,6 @@ let collect_vars sigma c = | _ -> EConstr.fold sigma aux vars c in aux Id.Set.empty c -let vars_of_global_reference = vars_of_global - (* Tests whether [m] is a subterm of [t]: [m] is appropriately lifted through abstractions of [t] *) @@ -1417,10 +1403,6 @@ let prod_applist_assum sigma n c l = | _ -> anomaly (Pp.str "Not enough prod/let's.") in app n [] c l -let on_judgment = Environ.on_judgment -let on_judgment_value = Environ.on_judgment_value -let on_judgment_type = Environ.on_judgment_type - (* Cut a context ctx in 2 parts (ctx1,ctx2) with ctx1 containing k non let-in variables skips let-in's; let-in's in the middle are put in ctx2 *) let context_chop k ctx = diff --git a/engine/termops.mli b/engine/termops.mli index 1dd9941c5e..a9217b3586 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -16,12 +16,6 @@ open Constr open Environ open EConstr -(** printers *) -val pr_sort_family : Sorts.family -> Pp.t -[@@ocaml.deprecated "Use [Sorts.pr_sort_family]"] -val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t -[@@ocaml.deprecated "Use [Constr.debug_print_fix]"] - (** about contexts *) val push_rel_assum : Name.t Context.binder_annot * types -> env -> env val push_rels_assum : (Name.t Context.binder_annot * Constr.types) list -> env -> env @@ -84,12 +78,6 @@ val fold_constr_with_full_binders : Evd.evar_map -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b -val iter_constr_with_full_binders : Evd.evar_map -> - (rel_declaration -> 'a -> 'a) -> - ('a -> constr -> unit) -> 'a -> - constr -> unit -[@@ocaml.deprecated "Use [EConstr.iter_with_full_binders]."] - (**********************************************************************) val strip_head_cast : Evd.evar_map -> constr -> constr @@ -121,9 +109,6 @@ val count_occurrences : Evd.evar_map -> constr -> constr -> int val collect_metas : Evd.evar_map -> constr -> int list val collect_vars : Evd.evar_map -> constr -> Id.Set.t (** for visible vars only *) -val vars_of_global_reference : env -> GlobRef.t -> Id.Set.t -[@@ocaml.deprecated "Use [Environ.vars_of_global]"] - (* Substitution of metavariables *) type meta_value_map = (metavariable * Constr.constr) list val subst_meta : meta_value_map -> Constr.constr -> Constr.constr @@ -292,15 +277,6 @@ val is_Type : Evd.evar_map -> constr -> bool val reference_of_level : Evd.evar_map -> Univ.Level.t -> Libnames.qualid option -(** Combinators on judgments *) - -val on_judgment : ('a -> 'b) -> ('a, 'a) punsafe_judgment -> ('b, 'b) punsafe_judgment -[@@ocaml.deprecated "Use [Environ.on_judgment]."] -val on_judgment_value : ('c -> 'c) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment -[@@ocaml.deprecated "Use [Environ.on_judgment_value]."] -val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) punsafe_judgment -[@@ocaml.deprecated "Use [Environ.on_judgment_type]."] - (** {5 Debug pretty-printers} *) open Evd diff --git a/engine/uState.ml b/engine/uState.ml index aa14f66df6..adea78d4c9 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -116,8 +116,6 @@ let univ_entry ~poly uctx = Polymorphic_entry (nas, uctx) else Monomorphic_entry (context_set uctx) -let const_univ_entry = univ_entry - let of_context_set ctx = { empty with uctx_local = ctx } let subst ctx = ctx.uctx_univ_variables diff --git a/engine/uState.mli b/engine/uState.mli index a358813825..3df7f9e8e9 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -67,9 +67,6 @@ val context : t -> Univ.UContext.t val univ_entry : poly:bool -> t -> Entries.universes_entry (** Pick from {!context} or {!context_set} based on [poly]. *) -val const_univ_entry : poly:bool -> t -> Entries.universes_entry -[@@ocaml.deprecated "Use [univ_entry]."] - (** {5 Constraints handling} *) val drop_weak_constraints : bool ref diff --git a/engine/univGen.ml b/engine/univGen.ml index c310331b15..f1deb1bfaf 100644 --- a/engine/univGen.ml +++ b/engine/univGen.ml @@ -25,11 +25,6 @@ let new_univ_global () = let fresh_level () = Univ.Level.make (new_univ_global ()) -(* TODO: remove *) -let new_univ () = Univ.Universe.make (fresh_level ()) -let new_Type () = mkType (new_univ ()) -let new_Type_sort () = sort_of_univ (new_univ ()) - let fresh_instance auctx = let inst = Array.init (AUContext.size auctx) (fun _ -> fresh_level()) in let ctx = Array.fold_right LSet.add inst LSet.empty in @@ -83,10 +78,6 @@ let constr_of_monomorphic_global gr = Pp.(str "globalization of polymorphic reference " ++ Nametab.pr_global_env Id.Set.empty gr ++ str " would forget universes.") -let constr_of_global gr = constr_of_monomorphic_global gr - -let constr_of_global_univ = mkRef - let fresh_global_or_constr_instance env = function | IsConstr c -> c, ContextSet.empty | IsGlobal gr -> fresh_global_instance env gr @@ -99,34 +90,6 @@ let global_of_constr c = | Var id -> VarRef id, Instance.empty | _ -> raise Not_found -open Declarations - -let type_of_reference env r = - match r with - | VarRef id -> Environ.named_type id env, ContextSet.empty - - | ConstRef c -> - let cb = Environ.lookup_constant c env in - let ty = cb.const_type in - let auctx = Declareops.constant_polymorphic_context cb in - let inst, ctx = fresh_instance auctx in - Vars.subst_instance_constr inst ty, ctx - - | IndRef ind -> - let (mib, _ as specif) = Inductive.lookup_mind_specif env ind in - let auctx = Declareops.inductive_polymorphic_context mib in - let inst, ctx = fresh_instance auctx in - let ty = Inductive.type_of_inductive env (specif, inst) in - ty, ctx - - | ConstructRef (ind,_ as cstr) -> - let (mib,_ as specif) = Inductive.lookup_mind_specif env ind in - let auctx = Declareops.inductive_polymorphic_context mib in - let inst, ctx = fresh_instance auctx in - Inductive.type_of_constructor (cstr,inst) specif, ctx - -let type_of_global t = type_of_reference (Global.env ()) t - let fresh_sort_in_family = function | InSProp -> Sorts.sprop, ContextSet.empty | InProp -> Sorts.prop, ContextSet.empty @@ -135,11 +98,6 @@ let fresh_sort_in_family = function let u = fresh_level () in sort_of_univ (Univ.Universe.make u), ContextSet.singleton u -let new_sort_in_family sf = - fst (fresh_sort_in_family sf) - -let extend_context = Univ.extend_in_context_set - let new_global_univ () = let u = fresh_level () in (Univ.Universe.make u, ContextSet.singleton u) diff --git a/engine/univGen.mli b/engine/univGen.mli index b4598e10d0..34920e5620 100644 --- a/engine/univGen.mli +++ b/engine/univGen.mli @@ -24,16 +24,7 @@ val new_univ_id : unit -> univ_unique_id (** for the stm *) val new_univ_global : unit -> Level.UGlobal.t val fresh_level : unit -> Level.t -val new_univ : unit -> Universe.t -[@@ocaml.deprecated "Use [new_univ_level]"] -val new_Type : unit -> types -[@@ocaml.deprecated "Use [new_univ_level]"] -val new_Type_sort : unit -> Sorts.t -[@@ocaml.deprecated "Use [new_univ_level]"] - val new_global_univ : unit -> Universe.t in_universe_context_set -val new_sort_in_family : Sorts.family -> Sorts.t -[@@ocaml.deprecated "Use [fresh_sort_in_family]"] (** Build a fresh instance for a given context, its associated substitution and the instantiated constraints. *) @@ -66,27 +57,9 @@ val fresh_universe_context_set_instance : ContextSet.t -> (** Raises [Not_found] if not a global reference. *) val global_of_constr : constr -> GlobRef.t puniverses -val constr_of_global_univ : GlobRef.t puniverses -> constr -[@@ocaml.deprecated "Use [Constr.mkRef]"] - -val extend_context : 'a in_universe_context_set -> ContextSet.t -> - 'a in_universe_context_set -[@@ocaml.deprecated "Use [Univ.extend_in_context_set]"] - (** Create a fresh global in the global environment, without side effects. BEWARE: this raises an error on polymorphic constants/inductives: the constraints should be properly added to an evd. See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for the proper way to get a fresh copy of a polymorphic global reference. *) val constr_of_monomorphic_global : GlobRef.t -> constr - -val constr_of_global : GlobRef.t -> constr -[@@ocaml.deprecated "constr_of_global will crash on polymorphic constants,\ - use [constr_of_monomorphic_global] if the reference is guaranteed to\ - be monomorphic, [Evarutil.new_global] or [Tacmach.New.pf_constr_of_global] otherwise"] - -(** Returns the type of the global reference, by creating a fresh instance of polymorphic - references and computing their instantiated universe context. (side-effect on the - universe counter, use with care). *) -val type_of_global : GlobRef.t -> types in_universe_context_set -[@@ocaml.deprecated "use [Typeops.type_of_global]"] diff --git a/ide/coqide.ml b/ide/coqide.ml index aa9e150fd5..4f00be27a1 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -561,7 +561,7 @@ let update_status sn = | None -> "" | Some n -> ", proving " ^ n in - display ("Ready"^ (if nanoPG#get then ", [μPG]" else "") ^ path ^ name); + display ("Ready"^ (if microPG#get then ", [μPG]" else "") ^ path ^ name); Coq.return () in Coq.bind (Coq.status false) next @@ -1200,7 +1200,7 @@ let build_ui () = item "Help for μPG mode" ~label:"Help for μPG mode" ~callback:(fun _ -> on_current_term (fun sn -> sn.messages#default_route#clear; - sn.messages#default_route#add_string (NanoPG.get_documentation ()))); + sn.messages#default_route#add_string (MicroPG.get_documentation ()))); item "About Coq" ~label:"_About" ~stock:`ABOUT ~callback:MiscMenu.about ]; @@ -1234,7 +1234,7 @@ let build_ui () = let () = vbox#pack toolbar#coerce in (* Emacs/PG mode *) - NanoPG.init w notebook all_menus; + MicroPG.init w notebook all_menus; (* On tab switch, reset, update location *) let _ = notebook#connect#switch_page ~callback:(fun n -> @@ -1251,7 +1251,7 @@ let build_ui () = let () = refresh_notebook_pos () in let lower_hbox = GPack.hbox ~homogeneous:false ~packing:vbox#pack () in let () = lower_hbox#pack ~expand:true status#coerce in - let () = push_info ("Ready"^ if nanoPG#get then ", [μPG]" else "") in + let () = push_info ("Ready"^ if microPG#get then ", [μPG]" else "") in (* Location display *) let l = GMisc.label diff --git a/ide/ide.mllib b/ide/ide.mllib index ed6520f29f..f8e8ff48d6 100644 --- a/ide/ide.mllib +++ b/ide/ide.mllib @@ -30,5 +30,5 @@ CoqOps Wg_Command Session Coqide_ui -NanoPG +MicroPG Coqide diff --git a/ide/nanoPG.ml b/ide/microPG.ml index d85d87142c..25cab4638c 100644 --- a/ide/nanoPG.ml +++ b/ide/microPG.ml @@ -65,14 +65,27 @@ type 'c entry = { } let mC = [`CONTROL] -let mM = [`MOD1] +let mM = + if Coq_config.arch = "Darwin" then + (* We add both MOD2 and META because both are + returned when pressing Command on MacOS X *) + [`CONTROL;`MOD2;`META] + else + [`MOD1] -let mod_of t x = List.for_all (fun m -> List.mem m (GdkEvent.Key.state t)) x +let mod_of t x = + let y = GdkEvent.Key.state t in + List.for_all (fun m -> List.mem m y) x && + List.for_all (fun m -> List.mem m x) y let pr_keymod l = - if l = mC then "C-" - else if l = mM then "M-" - else "" + if l = mC then + "Ctrl-" + else + if l = mM then + if Coq_config.arch = "Darwin" then "Ctrl-Cmd-" else "Meta-" + else + "" let mkE ?(mods=mC) key keyname doc ?(alias=[]) contents = List.map (fun (mods, key, keyname) -> { mods; key; keyname; doc; contents }) @@ -147,6 +160,13 @@ let emacs = insert emacs "Emacs" [] [ mkE _e "e" "Move to end of line" (Motion(fun s i -> (if not i#ends_line then i#forward_to_line_end else i), { s with move = None })); + mkE ~mods:mM _Right "->" "Move to end of buffer" (Motion(fun s i -> + i#forward_to_end, + { s with move = None })); + mkE ~mods:mM _Left "<-" "Move to start of buffer" (Motion(fun s i -> + let buffer = new GText.buffer i#buffer in + buffer#start_iter, + { s with move = None })); mkE _a "a" "Move to beginning of line" (Motion(fun s i -> (i#set_line_offset 0), { s with move = None })); mkE ~mods:mM _e "e" "Move to end of sentence" (Motion(fun s i -> @@ -286,9 +306,9 @@ let find gui (Step(here,konts)) t = else if k = _c && mod_of t mC && sel_nonempty () then ignore(run t gui (Action("Edit","Copy")) empty); - let cmp { key; mods } = key = k && mod_of t mods in - try `Do (List.find cmp here) with Not_found -> - try `Cont (List.find cmp konts).contents with Not_found -> `NotFound + let cmp { key; mods } = key = k && mod_of t mods in + try `Do (List.find cmp here) with Not_found -> + try `Cont (List.find cmp konts).contents with Not_found -> `NotFound let init w nb ags = let gui = { notebook = nb; action_groups = ags } in @@ -305,7 +325,7 @@ let init w nb ags = then false else begin eprintf "got key %s\n%!" (pr_key t); - if nanoPG#get then begin + if microPG#get then begin match find gui !cur t with | `Do e -> eprintf "run (%s) %s on %s\n%!" e.keyname e.doc (pr_status !status); @@ -320,4 +340,6 @@ let init w nb ags = -let get_documentation () = print_keypaths pg +let get_documentation () = + "Chars, words, lines and sentences below pertain to standard unicode segmentation rules\n" ^ + print_keypaths pg diff --git a/ide/nanoPG.mli b/ide/microPG.mli index bc9b39d823..bc9b39d823 100644 --- a/ide/nanoPG.mli +++ b/ide/microPG.mli diff --git a/ide/preferences.ml b/ide/preferences.ml index 3893d023bd..4e2e3f31e6 100644 --- a/ide/preferences.ml +++ b/ide/preferences.ml @@ -561,7 +561,8 @@ let tab_length = let highlight_current_line = new preference ~name:["highlight_current_line"] ~init:false ~repr:Repr.(bool) -let nanoPG = +let microPG = + (* Legacy name in preference is "nanoPG" *) new preference ~name:["nanoPG"] ~init:false ~repr:Repr.(bool) let user_queries = @@ -799,7 +800,7 @@ let configure ?(apply=(fun () -> ())) parent = let () = button "Show progress bar" show_progress_bar in let () = button "Insert spaces instead of tabs" spaces_instead_of_tabs in let () = button "Highlight current line" highlight_current_line in - let () = button "Emacs/PG keybindings (μPG mode)" nanoPG in + let () = button "Emacs/PG keybindings (μPG mode)" microPG in let callback () = () in custom ~label box callback true in diff --git a/ide/preferences.mli b/ide/preferences.mli index 785c191b46..b01c4598d8 100644 --- a/ide/preferences.mli +++ b/ide/preferences.mli @@ -102,7 +102,7 @@ val show_progress_bar : bool preference val spaces_instead_of_tabs : bool preference val tab_length : int preference val highlight_current_line : bool preference -val nanoPG : bool preference +val microPG : bool preference val user_queries : (string * string) list preference val diffs : string preference diff --git a/interp/constrextern.ml b/interp/constrextern.ml index e5bf52571c..bb66658a37 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -850,10 +850,10 @@ let rec extern inctx scopes vars r = | Some c :: q -> match locs with | [] -> anomaly (Pp.str "projections corruption [Constrextern.extern].") - | (_, false) :: locs' -> + | { Recordops.pk_true_proj = false } :: locs' -> (* we don't want to print locals *) ip q locs' args acc - | (_, true) :: locs' -> + | { Recordops.pk_true_proj = true } :: locs' -> match args with | [] -> raise No_match (* we give up since the constructor is not complete *) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index c0801067ce..f06493b374 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1368,7 +1368,7 @@ let sort_fields ~complete loc fields completer = let first_field = GlobRef.equal field_glob_ref first_field_glob_ref in begin match proj_kinds with | [] -> anomaly (Pp.str "Number of projections mismatch.") - | (_, regular) :: proj_kinds -> + | { Recordops.pk_true_proj = regular } :: proj_kinds -> (* "regular" is false when the field is defined by a let-in in the record declaration (its value is fixed from other fields). *) diff --git a/interp/impargs.ml b/interp/impargs.ml index d83a0ce918..90fb5a2036 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -120,8 +120,6 @@ let argument_position_eq p1 p2 = match p1, p2 with | Hyp h1, Hyp h2 -> Int.equal h1 h2 | _ -> false -let explicitation_eq = Constrexpr_ops.explicitation_eq - type implicit_explanation = | DepRigid of argument_position | DepFlex of argument_position diff --git a/interp/impargs.mli b/interp/impargs.mli index 0070423530..ccdd448460 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -143,7 +143,3 @@ val projection_implicits : env -> Projection.t -> implicit_status list -> val select_impargs_size : int -> implicits_list list -> implicit_status list val select_stronger_impargs : implicits_list list -> implicit_status list - -val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool - [@@ocaml.deprecated "Use Constrexpr_ops.explicitation_eq instead (since 8.10)"] -(** Equality on [explicitation]. *) diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 009eb3da38..bb3b0a538e 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -49,20 +49,6 @@ let weaker_noccur_between env x nvars t = (************************************************************************) (* Various well-formedness check for inductive declarations *) -(* Errors related to inductive constructions *) -type inductive_error = Type_errors.inductive_error = - | NonPos of env * constr * constr - | NotEnoughArgs of env * constr * constr - | NotConstructor of env * Id.t * constr * constr * int * int - | NonPar of env * constr * int * constr * constr - | SameNamesTypes of Id.t - | SameNamesConstructors of Id.t - | SameNamesOverlap of Id.t list - | NotAnArity of env * constr - | BadEntry - | LargeNonPropInductiveNotInType - | BadUnivs - exception InductiveError = Type_errors.InductiveError (************************************************************************) @@ -84,6 +70,7 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum let explain_ind_err id ntyp env nparamsctxt c err = + let open Type_errors in let (_lparams,c') = mind_extract_params nparamsctxt c in match err with | LocalNonPos kt -> @@ -329,7 +316,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( | Prod (na,b,d) -> let () = assert (List.is_empty largs) in if not recursive && not (noccur_between n ntypes b) then - raise (InductiveError BadEntry); + raise (InductiveError Type_errors.BadEntry); let nmr',recarg = check_pos ienv nmr b in let ienv' = ienv_push_var ienv (na,b,mk_norec) in check_constr_rec ienv' nmr' (recarg::lrec) d diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 7810c1723e..1b8e4208ff 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -9,28 +9,9 @@ (************************************************************************) open Names -open Constr open Declarations open Environ open Entries (** Check an inductive. *) val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body - -(** Deprecated *) -type inductive_error = - | NonPos of env * constr * constr - | NotEnoughArgs of env * constr * constr - | NotConstructor of env * Id.t * constr * constr * int * int - | NonPar of env * constr * int * constr * constr - | SameNamesTypes of Id.t - | SameNamesConstructors of Id.t - | SameNamesOverlap of Id.t list - | NotAnArity of env * constr - | BadEntry - | LargeNonPropInductiveNotInType - | BadUnivs -[@@ocaml.deprecated "Use [Type_errors.inductive_error]"] - -exception InductiveError of Type_errors.inductive_error -[@@ocaml.deprecated "Use [Type_errors.InductiveError]"] diff --git a/kernel/names.ml b/kernel/names.ml index 9f27212967..047a1d6525 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -376,9 +376,6 @@ module KerName = struct { modpath; knlabel; refhash = -1; } let repr kn = (kn.modpath, kn.knlabel) - let make2 = make - [@@ocaml.deprecated "Please use [KerName.make]"] - let modpath kn = kn.modpath let label kn = kn.knlabel diff --git a/kernel/names.mli b/kernel/names.mli index 61df3bad0e..2238e932b0 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -278,9 +278,6 @@ sig val make : ModPath.t -> Label.t -> t val repr : t -> ModPath.t * Label.t - val make2 : ModPath.t -> Label.t -> t - [@@ocaml.deprecated "Please use [KerName.make]"] - (** Projections *) val modpath : t -> ModPath.t val label : t -> Label.t diff --git a/lib/acyclicGraph.ml b/lib/acyclicGraph.ml index 7d04c8f5a1..e1dcfcc6ce 100644 --- a/lib/acyclicGraph.ml +++ b/lib/acyclicGraph.ml @@ -721,7 +721,10 @@ module Make (Point:Point) = struct let rmap, csts = PSet.fold (fun u (rmap,csts) -> let arcu = repr g u in if PSet.mem arcu.canon kept then - PMap.add arcu.canon arcu.canon rmap, Constraint.add (u,Eq,arcu.canon) csts + let csts = if Point.equal u arcu.canon then csts + else Constraint.add (u,Eq,arcu.canon) csts + in + PMap.add arcu.canon arcu.canon rmap, csts else match PMap.find arcu.canon rmap with | v -> rmap, Constraint.add (u,Eq,v) csts diff --git a/lib/rtree.ml b/lib/rtree.ml index e1c6a4c4d6..66d9eba3f7 100644 --- a/lib/rtree.ml +++ b/lib/rtree.ml @@ -115,8 +115,6 @@ struct end -let smartmap = Smart.map - (** Structural equality test, parametrized by an equality on elements *) let rec raw_eq cmp t t' = match t, t' with @@ -149,9 +147,6 @@ let equiv cmp cmp' = let equal cmp t t' = t == t' || raw_eq cmp t t' || equiv cmp cmp t t' -(** Deprecated alias *) -let eq_rtree = equal - (** Intersection of rtrees of same arity *) let rec inter cmp interlbl def n histo t t' = try diff --git a/lib/rtree.mli b/lib/rtree.mli index 5ab14f6039..67519aa387 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -77,15 +77,9 @@ val incl : ('a -> 'a -> bool) -> ('a -> 'a -> 'a option) -> 'a -> 'a t -> 'a t - (** See also [Smart.map] *) val map : ('a -> 'b) -> 'a t -> 'b t -val smartmap : ('a -> 'a) -> 'a t -> 'a t -(** @deprecated Same as [Smart.map] *) - (** A rather simple minded pretty-printer *) val pp_tree : ('a -> Pp.t) -> 'a t -> Pp.t -val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool -(** @deprecated Same as [Rtree.equal] *) - module Smart : sig diff --git a/library/global.ml b/library/global.ml index 55aed1c56e..06e06a8cf2 100644 --- a/library/global.ml +++ b/library/global.ml @@ -157,11 +157,6 @@ let import c u d = globalize (Safe_typing.import c u d) let env_of_context hyps = reset_with_named_context hyps (env()) -let type_of_global_in_context = Typeops.type_of_global_in_context - -let universes_of_global gr = - universes_of_global (env ()) gr - let is_polymorphic r = Environ.is_polymorphic (env()) r let is_template_polymorphic r = is_template_polymorphic (env ()) r diff --git a/library/global.mli b/library/global.mli index 76ac3f6279..a60de48897 100644 --- a/library/global.mli +++ b/library/global.mli @@ -131,14 +131,6 @@ val is_polymorphic : GlobRef.t -> bool val is_template_polymorphic : GlobRef.t -> bool val is_type_in_type : GlobRef.t -> bool -val type_of_global_in_context : Environ.env -> - GlobRef.t -> Constr.types * Univ.AUContext.t - [@@ocaml.deprecated "alias of [Typeops.type_of_global_in_context]"] - -(** Returns the universe context of the global reference (whatever its polymorphic status is). *) -val universes_of_global : GlobRef.t -> Univ.AUContext.t -[@@ocaml.deprecated "Use [Environ.universes_of_global]"] - (** {6 Retroknowledge } *) val register_inline : Constant.t -> unit diff --git a/library/globnames.ml b/library/globnames.ml index db2e8bfaed..99dcc43ad1 100644 --- a/library/globnames.ml +++ b/library/globnames.ml @@ -85,15 +85,6 @@ let printable_constr_of_global = function | ConstructRef sp -> mkConstruct sp | IndRef sp -> mkInd sp -module RefOrdered = Names.GlobRef.Ordered -module RefOrdered_env = Names.GlobRef.Ordered_env - -module Refmap = Names.GlobRef.Map -module Refset = Names.GlobRef.Set - -module Refmap_env = Names.GlobRef.Map_env -module Refset_env = Names.GlobRef.Set_env - (* Extended global references *) type syndef_name = KerName.t @@ -134,6 +125,3 @@ end type global_reference_or_constr = | IsGlobal of global_reference | IsConstr of constr - -(* Deprecated *) -let eq_gr = GlobRef.equal diff --git a/library/globnames.mli b/library/globnames.mli index d49ed453f5..14e422b743 100644 --- a/library/globnames.mli +++ b/library/globnames.mli @@ -25,8 +25,6 @@ val isConstRef : GlobRef.t -> bool val isIndRef : GlobRef.t -> bool val isConstructRef : GlobRef.t -> bool -val eq_gr : GlobRef.t -> GlobRef.t -> bool -[@@ocaml.deprecated "Use Names.GlobRef.equal"] val canonical_gr : GlobRef.t -> GlobRef.t val destVarRef : GlobRef.t -> variable @@ -48,22 +46,6 @@ val printable_constr_of_global : GlobRef.t -> constr raise [Not_found] if not a global reference *) val global_of_constr : constr -> GlobRef.t -module RefOrdered = Names.GlobRef.Ordered -[@@ocaml.deprecated "Use Names.GlobRef.Ordered"] - -module RefOrdered_env = Names.GlobRef.Ordered_env -[@@ocaml.deprecated "Use Names.GlobRef.Ordered_env"] - -module Refset = Names.GlobRef.Set -[@@ocaml.deprecated "Use Names.GlobRef.Set"] -module Refmap = Names.GlobRef.Map -[@@ocaml.deprecated "Use Names.GlobRef.Map"] - -module Refset_env = GlobRef.Set_env -[@@ocaml.deprecated "Use Names.GlobRef.Set_env"] -module Refmap_env = GlobRef.Map_env -[@@ocaml.deprecated "Use Names.GlobRef.Map_env"] - (** {6 Extended global references } *) type syndef_name = KerName.t diff --git a/library/lib.ml b/library/lib.ml index d4381a6923..a046360822 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -278,7 +278,7 @@ let start_mod is_type export id mp fs = let prefix = Nametab.{ obj_dir = dir; obj_mp = mp; obj_sec = Names.DirPath.empty } in let exists = if is_type then Nametab.exists_cci (make_path id) - else Nametab.exists_module dir + else Nametab.exists_dir dir in if exists then user_err ~hdr:"open_module" (Id.print id ++ str " already exists"); @@ -569,7 +569,7 @@ let open_section id = let opp = !lib_state.path_prefix in let obj_dir = add_dirpath_suffix opp.Nametab.obj_dir id in let prefix = Nametab.{ obj_dir; obj_mp = opp.obj_mp; obj_sec = add_dirpath_suffix opp.obj_sec id } in - if Nametab.exists_section obj_dir then + if Nametab.exists_dir obj_dir then user_err ~hdr:"open_section" (Id.print id ++ str " already exists."); let fs = Summary.freeze_summaries ~marshallable:false in add_entry (make_foname id) (OpenedSection (prefix, fs)); diff --git a/library/nametab.ml b/library/nametab.ml index 95890b2edf..bd0ea5f04f 100644 --- a/library/nametab.ml +++ b/library/nametab.ml @@ -43,12 +43,6 @@ module GlobDirRef = struct end -type global_dir_reference = GlobDirRef.t -[@@ocaml.deprecated "Use [GlobDirRef.t]"] - -let eq_global_dir_reference = GlobDirRef.equal -[@@ocaml.deprecated "Use [GlobDirRef.equal]"] - exception GlobalizationError of qualid let error_global_not_found qid = @@ -516,10 +510,6 @@ let exists_cci sp = ExtRefTab.exists sp !the_ccitab let exists_dir dir = DirTab.exists dir !the_dirtab -let exists_section = exists_dir - -let exists_module = exists_dir - let exists_modtype sp = MPTab.exists sp !the_modtypetab let exists_universe kn = UnivTab.exists kn !the_univtab @@ -585,10 +575,3 @@ let global_inductive qid = | ref -> user_err ?loc:qid.CAst.loc ~hdr:"global_inductive" (pr_qualid qid ++ spc () ++ str "is not an inductive type") - -(********************************************************************) - -(* Deprecated synonyms *) - -let extended_locate = locate_extended -let absolute_reference = global_of_path diff --git a/library/nametab.mli b/library/nametab.mli index fccb8fd918..a4f177aad0 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -89,13 +89,6 @@ module GlobDirRef : sig val equal : t -> t -> bool end -type global_dir_reference = GlobDirRef.t -[@@ocaml.deprecated "Use [GlobDirRef.t]"] - -val eq_global_dir_reference : - GlobDirRef.t -> GlobDirRef.t -> bool -[@@ocaml.deprecated "Use [GlobDirRef.equal]"] - exception GlobalizationError of qualid (** Raises a globalization error *) @@ -170,10 +163,6 @@ val extended_global_of_path : full_path -> extended_global_reference val exists_cci : full_path -> bool val exists_modtype : full_path -> bool val exists_dir : DirPath.t -> bool -val exists_section : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) - -val exists_module : DirPath.t -> bool (** deprecated synonym of [exists_dir] *) - val exists_universe : full_path -> bool (** {6 These functions locate qualids into full user names } *) @@ -220,11 +209,6 @@ val shortest_qualid_of_modtype : ?loc:Loc.t -> ModPath.t -> qualid val shortest_qualid_of_module : ?loc:Loc.t -> ModPath.t -> qualid val shortest_qualid_of_universe : ?loc:Loc.t -> Univ.Level.UGlobal.t -> qualid -(** Deprecated synonyms *) - -val extended_locate : qualid -> extended_global_reference (*= locate_extended *) -val absolute_reference : full_path -> GlobRef.t (** = global_of_path *) - (** {5 Generic name handling} *) (** NOT FOR PUBLIC USE YET. Plugin writers, please do not rely on this API. *) diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 3dd3a430e8..1fca132655 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -132,7 +132,7 @@ let nat = function () -> (coq_init_constant "nat") let iter_ref () = try find_reference ["Recdef"] "iter" with Not_found -> user_err Pp.(str "module Recdef not loaded") -let iter_rd = function () -> (constr_of_global (delayed_force iter_ref)) +let iter_rd = function () -> (constr_of_monomorphic_global (delayed_force iter_ref)) let eq = function () -> (coq_init_constant "eq") let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS") let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm") @@ -145,7 +145,7 @@ let coq_O = function () -> (coq_init_constant "O") let coq_S = function () -> (coq_init_constant "S") let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r") let max_ref = function () -> (find_reference ["Recdef"] "max") -let max_constr = function () -> EConstr.of_constr (constr_of_global (delayed_force max_ref)) +let max_constr = function () -> EConstr.of_constr (constr_of_monomorphic_global (delayed_force max_ref)) let f_S t = mkApp(delayed_force coq_S, [|t|]);; @@ -1041,13 +1041,13 @@ let compute_terminate_type nb_args func = let open Term in let open Constr in let open CVars in - let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_global func)) in + let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_monomorphic_global func)) in let rev_args,b = decompose_prod_n nb_args a_arrow_b in let left = mkApp(delayed_force iter_rd, Array.of_list (lift 5 a_arrow_b:: mkRel 3:: - constr_of_global func::mkRel 1:: + constr_of_monomorphic_global func::mkRel 1:: List.rev (List.map_i (fun i _ -> mkRel (6+i)) 0 rev_args) ) ) @@ -1065,7 +1065,7 @@ let compute_terminate_type nb_args func = delayed_force nat, (mkProd (make_annot (Name k_id) Sorts.Relevant, delayed_force nat, mkArrow cond Sorts.Relevant result))))|])in - let value = mkApp(constr_of_global (Util.delayed_force coq_sig_ref), + let value = mkApp(constr_of_monomorphic_global (Util.delayed_force coq_sig_ref), [|b; (mkLambda (make_annot (Name v_id) Sorts.Relevant, b, nb_iter))|]) in compose_prod rev_args value @@ -1161,7 +1161,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a fun g -> let sigma = project g in let ids = Termops.ids_of_named_context (pf_hyps g) in - let func_body = (def_of_const (constr_of_global func)) in + let func_body = (def_of_const (constr_of_monomorphic_global func)) in let func_body = EConstr.of_constr func_body in let (f_name, _, body1) = destLambda sigma func_body in let f_id = @@ -1222,7 +1222,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a let get_current_subgoals_types pstate = let p = Proof_global.give_me_the_proof pstate in - let sgs,_,_,_,sigma = Proof.proof p in + let Proof.{ goals=sgs; sigma; _ } = Proof.data p in sigma, List.map (Goal.V82.abstract_type sigma) sgs exception EmptySubgoals @@ -1253,7 +1253,7 @@ let build_and_l sigma l = let c,tac,nb = f pl in mk_and p1 c, tclTHENS - (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_global conj_constr)))) + (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_monomorphic_global conj_constr)))) [tclIDTAC; tac ],nb+1 @@ -1437,7 +1437,7 @@ let start_equation (f:GlobRef.t) (term_f:GlobRef.t) (cont_tactic:Id.t list -> tactic) g = let sigma = project g in let ids = pf_ids_of_hyps g in - let terminate_constr = constr_of_global term_f in + let terminate_constr = constr_of_monomorphic_global term_f in let terminate_constr = EConstr.of_constr terminate_constr in let nargs = nb_prod (project g) (EConstr.of_constr (type_of_const sigma terminate_constr)) in let x = n_x_id ids nargs in @@ -1457,7 +1457,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation | _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.") in let evd = Evd.from_ctx uctx in - let f_constr = constr_of_global f_ref in + let f_constr = constr_of_monomorphic_global f_ref in let equation_lemma_type = subst1 f_constr equation_lemma_type in let pstate = Lemmas.start_proof ~ontop:None eq_name (Global, false, Proof Lemma) ~sign evd (EConstr.of_constr equation_lemma_type) in @@ -1466,12 +1466,12 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation (fun x -> prove_eq (fun _ -> tclIDTAC) {nb_arg=nb_arg; - f_terminate = EConstr.of_constr (constr_of_global terminate_ref); + f_terminate = EConstr.of_constr (constr_of_monomorphic_global terminate_ref); f_constr = EConstr.of_constr f_constr; concl_tac = tclIDTAC; func=functional_ref; info=(instantiate_lambda Evd.empty - (EConstr.of_constr (def_of_const (constr_of_global functional_ref))) + (EConstr.of_constr (def_of_const (constr_of_monomorphic_global functional_ref))) (EConstr.of_constr f_constr::List.map mkVar x) ); is_main_branch = true; @@ -1570,9 +1570,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num if not stop then let eq_ref = Nametab.locate (qualid_of_ident equation_id ) in - let f_ref = destConst (constr_of_global f_ref) - and functional_ref = destConst (constr_of_global functional_ref) - and eq_ref = destConst (constr_of_global eq_ref) in + let f_ref = destConst (constr_of_monomorphic_global f_ref) + and functional_ref = destConst (constr_of_monomorphic_global functional_ref) + and eq_ref = destConst (constr_of_monomorphic_global eq_ref) in generate_induction_principle f_ref tcc_lemma_constr functional_ref eq_ref rec_arg_num (EConstr.of_constr rec_arg_type) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index ef6af16036..de9dec0f74 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -207,7 +207,7 @@ struct * ZMicromega.v *) - let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n) + let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules s m n) let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules [@@@ocaml.warning "+3"] diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index e349031952..93c0d5c236 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -446,7 +446,7 @@ let lz_setoid_relation = | Some (env', srel) when env' == env -> srel | _ -> let srel = - try Some (UnivGen.constr_of_global @@ + try Some (UnivGen.constr_of_monomorphic_global @@ Coqlib.find_reference "Class_setoid" ("Coq"::sdir) "RewriteRelation" [@ocaml.warning "-3"]) with _ -> None in last_srel := Some (env, srel); srel @@ -491,7 +491,7 @@ let rwprocess_rule dir rule gl = | _ -> let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in EConstr.mkApp (pi2, ra), sigma in - if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.True.type"))) then + if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.True.type"))) then let s, sigma = sr sigma 2 in loop (converse_dir d) sigma s a.(1) rs 0 else diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 99013a19c9..6b149a8b41 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -1769,28 +1769,3 @@ let unify ?flags ?(with_ho=true) env evd cv_pb ty1 ty2 = solve_unif_constraints_with_heuristics ~flags ~with_ho env evd | UnifFailure (evd, reason) -> raise (PretypeError (env, evd, CannotUnify (ty1, ty2, Some reason))) - -(* deprecated *) -let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd = - let flags = default_flags_of ts in - match evar_conv_x flags env evd CONV t1 t2 with - | Success evd' -> evd' - | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) - -let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd = - let flags = default_flags_of ts in - match evar_conv_x flags env evd CUMUL t1 t2 with - | Success evd' -> evd' - | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) - -let make_opt = function - | Success evd -> Some evd - | UnifFailure _ -> None - -let conv env ?(ts=default_transparent_state env) evd t1 t2 = - let flags = default_flags_of ts in - make_opt(evar_conv_x flags env evd CONV t1 t2) - -let cumul env ?(ts=default_transparent_state env) evd t1 t2 = - let flags = default_flags_of ts in - make_opt(evar_conv_x flags env evd CUMUL t1 t2) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index bf83f5e88f..eae961714d 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -46,19 +46,6 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error val unify_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map val unify_leq_delay : ?flags:unify_flags -> env -> evar_map -> constr -> constr -> evar_map -(** returns exception UnableToUnify with best known evar_map if not unifiable *) -val the_conv_x : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map -[@@ocaml.deprecated "Use Evarconv.unify_delay instead"] -val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map -[@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"] -(** The same function resolving evars by side-effect and - catching the exception *) - -val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option -[@@ocaml.deprecated "Use Evarconv.unify_delay instead"] -val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option -[@@ocaml.deprecated "Use Evarconv.unify_leq_delay instead"] - (** This function also calls [solve_unif_constraints_with_heuristics] to resolve any remaining constraints. In case of success the two terms are unified without condition. diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index d69824a256..a23c58c062 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -27,16 +27,27 @@ open Reductionops (*s A structure S is a non recursive inductive type with a single constructor (the name of which defaults to Build_S) *) -(* Table des structures: le nom de la structure (un [inductive]) donne - le nom du constructeur, le nombre de paramètres et pour chaque - argument réel du constructeur, le nom de la projection - correspondante, si valide, et un booléen disant si c'est une vraie - projection ou bien une fonction constante (associée à un LetIn) *) +(* Table of structures. + It maps to each structure name (of type [inductive]): + - the name of its constructor; + - the number of parameters; + - for each true argument, some data about the corresponding projection: + * its name (may be anonymous); + * whether it is a true projection (as opposed to a constant function, LetIn); + * whether it should be used as a canonical hint; + * the constant realizing this projection (if any). +*) + +type proj_kind = { + pk_name: Name.t; + pk_true_proj: bool; + pk_canonical: bool; +} type struc_typ = { s_CONST : constructor; s_EXPECTEDPARAM : int; - s_PROJKIND : (Name.t * bool) list; + s_PROJKIND : proj_kind list; s_PROJ : Constant.t option list } let structure_table = @@ -47,7 +58,7 @@ let projection_table = (* TODO: could be unify struc_typ and struc_tuple ? *) type struc_tuple = - constructor * (Name.t * bool) list * Constant.t option list + constructor * proj_kind list * Constant.t option list let register_structure env (id,kl,projs) = let open Declarations in @@ -161,7 +172,7 @@ let canonical_projections () = !object_table [] let keep_true_projections projs kinds = - let filter (p, (_, b)) = if b then Some p else None in + let filter (p, { pk_true_proj ; pk_canonical }) = if pk_true_proj then Some (p, pk_canonical) else None in List.map_filter filter (List.combine projs kinds) let rec cs_pattern_of_constr env t = @@ -206,17 +217,20 @@ let compute_canonical_projections env ~warn (con,ind) = let o_NPARAMS = List.length o_TPARAMS in let lpj = keep_true_projections lpj kl in let nenv = Termops.push_rels_assum sign env in - List.fold_left2 (fun acc spopt t -> - Option.cata (fun proji_sp -> - match cs_pattern_of_constr nenv t with - | patt, o_INJ, o_TCOMPS -> - ((ConstRef proji_sp, (patt, t)), - { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) - :: acc - | exception Not_found -> - if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp); - acc - ) acc spopt + List.fold_left2 (fun acc (spopt, canonical) t -> + if canonical + then + Option.cata (fun proji_sp -> + match cs_pattern_of_constr nenv t with + | patt, o_INJ, o_TCOMPS -> + ((ConstRef proji_sp, (patt, t)), + { o_DEF ; o_CTX ; o_INJ ; o_TABS ; o_TPARAMS ; o_NPARAMS ; o_TCOMPS }) + :: acc + | exception Not_found -> + if warn then warn_projection_no_head_constant (sign, env, t, con, proji_sp); + acc + ) acc spopt + else acc ) [] lpj projs let pr_cs_pattern = function @@ -288,7 +302,7 @@ let check_and_decompose_canonical_structure env sigma ref = with Not_found -> error_not_structure ref (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env sigma (EConstr.mkInd indsp)) in - let ntrue_projs = List.count snd s.s_PROJKIND in + let ntrue_projs = List.count (fun { pk_true_proj } -> pk_true_proj) s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then error_not_structure ref (str "Got too few arguments to the record or structure constructor."); (sp,indsp) diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index f0594d513a..25b6cd0751 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -17,14 +17,20 @@ open Constr (** A structure S is a non recursive inductive type with a single constructor (the name of which defaults to Build_S) *) +type proj_kind = { + pk_name: Name.t; + pk_true_proj: bool; + pk_canonical: bool; +} + type struc_typ = { s_CONST : constructor; s_EXPECTEDPARAM : int; - s_PROJKIND : (Name.t * bool) list; + s_PROJKIND : proj_kind list; s_PROJ : Constant.t option list } type struc_tuple = - constructor * (Name.t * bool) list * Constant.t option list + constructor * proj_kind list * Constant.t option list val register_structure : Environ.env -> struc_tuple -> unit val subst_structure : Mod_subst.substitution -> struc_tuple -> struc_tuple diff --git a/printing/printmod.ml b/printing/printmod.ml index f4986652b3..bd97104f60 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -63,7 +63,7 @@ let keyword s = tag_keyword (str s) let get_new_id locals id = let rec get_id l id = let dir = DirPath.make [id] in - if not (Nametab.exists_module dir) then + if not (Nametab.exists_dir dir) then id else get_id (Id.Set.add id l) (Namegen.next_ident_away id l) diff --git a/proofs/proof.ml b/proofs/proof.ml index 978b1f6f78..778d98b2cd 100644 --- a/proofs/proof.ml +++ b/proofs/proof.ml @@ -126,9 +126,6 @@ type t = (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *) } -let initial_goals pf = Proofview.initial_goals pf.entry -let initial_euctx pf = pf.initial_euctx - (*** General proof functions ***) let proof p = @@ -147,33 +144,6 @@ let proof p = let given_up = p.given_up in (goals,stack,shelf,given_up,sigma) -type 'a pre_goals = { - fg_goals : 'a list; - (** List of the focussed goals *) - bg_goals : ('a list * 'a list) list; - (** Zipper representing the unfocussed background goals *) - shelved_goals : 'a list; - (** List of the goals on the shelf. *) - given_up_goals : 'a list; - (** List of the goals that have been given up *) -} - -let map_structured_proof pfts process_goal: 'a pre_goals = - let (goals, zipper, shelf, given_up, sigma) = proof pfts in - let fg = List.map (process_goal sigma) goals in - let map_zip (lg, rg) = - let lg = List.map (process_goal sigma) lg in - let rg = List.map (process_goal sigma) rg in - (lg, rg) - in - let bg = List.map map_zip zipper in - let shelf = List.map (process_goal sigma) shelf in - let given_up = List.map (process_goal sigma) given_up in - { fg_goals = fg; - bg_goals = bg; - shelved_goals = shelf; - given_up_goals = given_up; } - let rec unroll_focus pv = function | (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk | [] -> pv @@ -441,22 +411,6 @@ let in_proof p k = k (Proofview.return p.proofview) let unshelve p = { p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] } -let pr_proof p = - let p = map_structured_proof p (fun _sigma g -> g) in - Pp.( - let pr_goal_list = prlist_with_sep spc Goal.pr_goal in - let rec aux acc = function - | [] -> acc - | (before,after)::stack -> - aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++ - pr_goal_list after) stack in - str "[" ++ str "focus structure: " ++ - aux (pr_goal_list p.fg_goals) p.bg_goals ++ str ";" ++ spc () ++ - str "shelved: " ++ pr_goal_list p.shelved_goals ++ str ";" ++ spc () ++ - str "given up: " ++ pr_goal_list p.given_up_goals ++ - str "]" - ) - (*** Compatibility layer with <=v8.2 ***) module V82 = struct @@ -554,3 +508,19 @@ let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name; let stack = map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in { sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly } + +let pr_proof p = + let { goals=fg_goals; stack=bg_goals; shelf; given_up; _ } = data p in + Pp.( + let pr_goal_list = prlist_with_sep spc Goal.pr_goal in + let rec aux acc = function + | [] -> acc + | (before,after)::stack -> + aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++ + pr_goal_list after) stack in + str "[" ++ str "focus structure: " ++ + aux (pr_goal_list fg_goals) bg_goals ++ str ";" ++ spc () ++ + str "shelved: " ++ pr_goal_list shelf ++ str ";" ++ spc () ++ + str "given up: " ++ pr_goal_list given_up ++ + str "]" + ) diff --git a/proofs/proof.mli b/proofs/proof.mli index defef57a8d..1f4748141a 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -34,30 +34,6 @@ (* Type of a proof. *) type t -(* Returns a stylised view of a proof for use by, for instance, - ide-s. *) -(* spiwack: the type of [proof] will change as we push more refined - functions to ide-s. This would be better than spawning a new nearly - identical function everytime. Hence the generic name. *) -(* In this version: returns the focused goals, a representation of the - focus stack (the goals at each level), a representation of the - shelf (the list of goals on the shelf), a representation of the - given up goals (the list of the given up goals) and the underlying - evar_map *) -val proof : t -> - Goal.goal list - * (Goal.goal list * Goal.goal list) list - * Goal.goal list - * Goal.goal list - * Evd.evar_map -[@@ocaml.deprecated "use [Proof.data]"] - -val initial_goals : t -> (EConstr.constr * EConstr.types) list -[@@ocaml.deprecated "use [Proof.data]"] - -val initial_euctx : t -> UState.t -[@@ocaml.deprecated "use [Proof.data]"] - type data = { sigma : Evd.evar_map (** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *) @@ -81,29 +57,6 @@ type data = val data : t -> data -(* Generic records structured like the return type of proof *) -type 'a pre_goals = { - fg_goals : 'a list; - [@ocaml.deprecated "use [Proof.data]"] - (** List of the focussed goals *) - bg_goals : ('a list * 'a list) list; - [@ocaml.deprecated "use [Proof.data]"] - (** Zipper representing the unfocussed background goals *) - shelved_goals : 'a list; - [@ocaml.deprecated "use [Proof.data]"] - (** List of the goals on the shelf. *) - given_up_goals : 'a list; - [@ocaml.deprecated "use [Proof.data]"] - (** List of the goals that have been given up *) -} -[@@ocaml.deprecated "use [Proof.data]"] - -(* needed in OCaml 4.05.0, not needed in newer ones *) -[@@@ocaml.warning "-3"] -val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) [@ocaml.warning "-3"] -[@@ocaml.deprecated "use [Proof.data]"] -[@@@ocaml.warning "+3"] - (*** General proof functions ***) val start : name:Names.Id.t diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 7b3d9e534b..93031c2202 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -104,10 +104,6 @@ let db_pr_goal sigma g = let pr_gls gls = hov 0 (pr_evar_map (Some 2) (pf_env gls) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls)) -let pr_glls glls = - hov 0 (pr_evar_map (Some 2) (Global.env()) (sig_sig glls) ++ fnl () ++ - prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls)) - (* Variants of [Tacmach] functions built with the new proof engine *) module New = struct diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 218011c316..23e1e6f566 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -68,8 +68,6 @@ val pf_conv_x_leq : Goal.goal sigma -> constr -> constr -> bool (** {6 Pretty-printing functions (debug only). } *) val pr_gls : Goal.goal sigma -> Pp.t -val pr_glls : Goal.goal list sigma -> Pp.t -[@@ocaml.deprecated "Please move to \"new\" proof engine"] (** Variants of [Tacmach] functions built with the new proof engine *) module New : sig diff --git a/tactics/ppred.mli b/tactics/ppred.mli index be21236f4e..c68fab5296 100644 --- a/tactics/ppred.mli +++ b/tactics/ppred.mli @@ -6,11 +6,6 @@ val pr_with_occurrences : val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t -val pr_red_expr : - ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> - (string -> Pp.t) -> ('a,'b,'c) red_expr_gen -> Pp.t - [@@ocaml.deprecated "Use pr_red_expr_env instead"] - val pr_red_expr_env : Environ.env -> Evd.evar_map -> (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * (Environ.env -> Evd.evar_map -> 'a -> Pp.t) * diff --git a/test-suite/dune b/test-suite/dune index c430400ba5..cd33319fa4 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -20,6 +20,8 @@ ../dev/header.ml ../dev/tools/update-compat.py ../doc/stdlib/index-list.html.template + ; For the changelog test + ../config/coq_config.py (package coq) ; For fake_ide (package coqide-server) diff --git a/test-suite/misc/changelog.sh b/test-suite/misc/changelog.sh new file mode 100755 index 0000000000..8b4a49e577 --- /dev/null +++ b/test-suite/misc/changelog.sh @@ -0,0 +1,18 @@ +#!/bin/sh + +while read line; do + if [ "$line" = "is_a_released_version = False" ]; then + echo "This is not a released version: nothing to test." + exit 0 + fi +done < ../config/coq_config.py + +for d in ../doc/changelog/*; do + if [ -d "$d" ]; then + if [ "$(ls $d/*.rst | wc -l)" != "1" ]; then + echo "Fatal: unreleased changelog entries remain in ${d#../}/" + echo "Include them in doc/sphinx/changes.rst and remove them from doc/changelog/" + exit 1 + fi + fi +done diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 9d972a68f7..c1b9a2b1c6 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -1,5 +1,15 @@ [< 0 > + < 1 > * < 2 >] : nat +Entry constr:myconstr is +[ "6" RIGHTA + [ ] +| "5" RIGHTA + [ SELF; "+"; NEXT ] +| "4" RIGHTA + [ SELF; "*"; NEXT ] +| "3" RIGHTA + [ "<"; constr:operconstr LEVEL "10"; ">" ] ] + [< b > + < b > * < 2 >] : nat [<< # 0 >>] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 81c64418cb..d1063bfd04 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -9,6 +9,7 @@ Notation "x + y" := (Nat.add x y) (in custom myconstr at level 5). Notation "x * y" := (Nat.mul x y) (in custom myconstr at level 4). Notation "< x >" := x (in custom myconstr at level 3, x constr at level 10). Check [ < 0 > + < 1 > * < 2 >]. +Print Custom Grammar myconstr. Axiom a : nat. Notation b := a. diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v index 2533a39cc4..d047f7560e 100644 --- a/test-suite/success/Notations2.v +++ b/test-suite/success/Notations2.v @@ -151,8 +151,8 @@ Module M16. Local Notation "##" := 0 (in custom foo2). (* Test Print Grammar *) - Print Grammar foo. - Print Grammar foo2. + Print Custom Grammar foo. + Print Custom Grammar foo2. End M16. (* Example showing the need for strong evaluation of diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v index f4f59a3c16..4717759dec 100644 --- a/test-suite/success/attribute_syntax.v +++ b/test-suite/success/attribute_syntax.v @@ -20,6 +20,10 @@ Check ι _ ι. Fixpoint f (n: nat) {wf lt n} : nat := _. Reset f. +#[program(true)] +Fixpoint f (n: nat) {wf lt n} : nat := _. +Reset f. + #[deprecated(since="8.9.0")] Ltac foo := foo. diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 9a18baa0bc..ec43dbb1d7 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -184,10 +184,6 @@ let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> Pp.strbrk "The inputstate option is deprecated and discouraged.") -let warn_deprecated_boot = - CWarnings.create ~name:"deprecated-boot" ~category:"noop" - (fun () -> Pp.strbrk "The -boot option is deprecated, please use -q and/or -coqlib options instead.") - let set_inputstate opts s = warn_deprecated_inputstate (); { opts with inputstate = Some s } @@ -488,9 +484,6 @@ let parse_args ~help ~init arglist : t * string list = { oval with batch = true } |"-test-mode" -> Vernacentries.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval - |"-boot" -> - warn_deprecated_boot (); - { oval with load_rcfile = false; } |"-bt" -> Backtrace.record_backtrace true; oval |"-color" -> set_color oval (next ()) |"-config"|"--config" -> { oval with print_config = true } diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 9323a57417..b769405cf6 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -271,31 +271,6 @@ let init_toploop opts = let state = { doc; sid; proof = None; time = opts.time } in Ccompile.load_init_vernaculars opts ~state, opts -(* To remove in 8.11 *) -let call_coqc args = - let remove str arr = Array.(of_list List.(filter (fun l -> not String.(equal l str)) (to_list arr))) in - let coqc_name = Filename.remove_extension (System.get_toplevel_path "coqc") in - let args = remove "-compile" args in - Unix.execv coqc_name args - -let deprecated_coqc_warning = CWarnings.(create - ~name:"deprecate-compile-arg" - ~category:"toplevel" - ~default:Enabled - (fun opt_name -> Pp.(seq [str "The option "; str opt_name; str" is deprecated, please use coqc."]))) - -let rec coqc_deprecated_check args acc extras = - match extras with - | [] -> acc - | "-o" :: _ :: rem -> - deprecated_coqc_warning "-o"; - coqc_deprecated_check args acc rem - | ("-compile"|"-compile-verbose") :: file :: rem -> - deprecated_coqc_warning "-compile"; - call_coqc args - | x :: rem -> - coqc_deprecated_check args (x::acc) rem - let coqtop_init ~opts extra = init_color opts; CoqworkmgrApi.(init !async_proofs_worker_priority); @@ -317,7 +292,6 @@ let start_coq custom = init_toplevel ~help:Usage.print_usage_coqtop ~init:default custom.init (List.tl (Array.to_list Sys.argv)) in - let extras = coqc_deprecated_check Sys.argv [] extras in if not (CList.is_empty extras) then begin prerr_endline ("Don't know what to do with "^String.concat " " extras); prerr_endline "See -help for the list of supported options"; diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 7074215afe..da2094653b 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -102,12 +102,6 @@ let print_usage_coqtop () = coqtop specific options:\ \n\ \n -batch batch mode (exits just after argument parsing)\ -\n\ -\nDeprecated options [use coqc instead]:\ -\n\ -\n -compile f.v compile Coq file f.v (implies -batch)\ -\n -compile-verbose f.v verbosely compile Coq file f.v (implies -batch)\ -\n -o f.vo use f.vo as the output file name\ \n"; flush stderr ; exit 1 @@ -128,14 +122,6 @@ coqc specific options:\ \nUndocumented:\ \n -vio2vo [see manual]\ \n -check-vio-tasks [see manual]\ -\n\ -\nDeprecated options:\ -\n\ -\n -image f specify an alternative executable for Coq\ -\n -opt run the native-code version of Coq\ -\n -byte run the bytecode version of Coq\ -\n -t keep temporary files\ -\n -outputstate file save summary state in file \ \n"; flush stderr ; exit 1 diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 9b8c4efb37..1ad5862d5d 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -82,9 +82,12 @@ let assert_empty k v = if v <> VernacFlagEmpty then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments") +let error_twice ~name : 'a = + user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.") + let assert_once ~name prev = if Option.has_some prev then - user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.") + error_twice ~name let attribute_of_list (l:(string * 'a key_parser) list) : 'a option attribute = let rec p extra v = function @@ -107,6 +110,24 @@ let bool_attribute ~name ~on ~off : bool option attribute = attribute_of_list [(on, single_key_parser ~name ~key:on true); (off, single_key_parser ~name ~key:off false)] +(* Variant of the [bool] attribute with only two values (bool has three). *) +let get_bool_value ~key ~default = + function + | VernacFlagEmpty -> default + | VernacFlagList [ "true", VernacFlagEmpty ] -> true + | VernacFlagList [ "false", VernacFlagEmpty ] -> false + | _ -> user_err Pp.(str "Attribute " ++ str key ++ str " only accepts boolean values.") + +let enable_attribute ~key ~default : bool attribute = + fun atts -> + let default = default () in + let this, extra = List.partition (fun (k, _) -> String.equal key k) atts in + extra, + match this with + | [] -> default + | [ _, value ] -> get_bool_value ~key ~default:true value + | _ -> error_twice ~name:key + let qualify_attribute qual (parser:'a attribute) : 'a attribute = fun atts -> let rec extract extra qualified = function @@ -139,11 +160,8 @@ let () = let open Goptions in optread = (fun () -> !program_mode); optwrite = (fun b -> program_mode:=b) } -let program_opt = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram" - -let program = program_opt >>= function - | Some b -> return b - | None -> return (!program_mode) +let program = + enable_attribute ~key:"program" ~default:(fun () -> !program_mode) let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global" @@ -219,3 +237,6 @@ let only_polymorphism atts = parse polymorphic atts let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty] let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty] + +let canonical = + enable_attribute ~key:"canonical" ~default:(fun () -> true) diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 3cb4d69ca0..44688ddafc 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -52,6 +52,7 @@ val program : bool attribute val template : bool option attribute val locality : bool option attribute val deprecation : deprecation option attribute +val canonical : bool attribute val program_mode_option_name : string list (** For internal use when messing with the global option. *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 59d2a66259..6438b48e32 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -43,6 +43,7 @@ let query_command = Entry.create "vernac:query_command" let subprf = Entry.create "vernac:subprf" +let quoted_attributes = Entry.create "vernac:quoted_attributes" let class_rawexpr = Entry.create "vernac:class_rawexpr" let thm_token = Entry.create "vernac:thm_token" let def_body = Entry.create "vernac:def_body" @@ -75,7 +76,7 @@ let parse_compat_version = let open Flags in function } GRAMMAR EXTEND Gram - GLOBAL: vernac_control gallina_ext noedit_mode subprf; + GLOBAL: vernac_control quoted_attributes gallina_ext noedit_mode subprf; vernac_control: FIRST [ [ IDENT "Time"; c = vernac_control -> { CAst.make ~loc @@ VernacTime (false,c) } | IDENT "Redirect"; s = ne_string; c = vernac_control -> { CAst.make ~loc @@ VernacRedirect (s, c) } @@ -447,10 +448,12 @@ GRAMMAR EXTEND Gram *) (* ... with coercions *) record_field: - [ [ bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ]; + [ [ attr = LIST0 quoted_attributes ; + bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ]; rf_notation = decl_notation -> { + let rf_canonical = attr |> List.flatten |> parse canonical in let rf_subclass, rf_decl = bd in - rf_decl, { rf_subclass ; rf_priority ; rf_notation } } ] ] + rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ] ; record_fields: [ [ f = record_field; ";"; fs = record_fields -> { f :: fs } @@ -1003,6 +1006,9 @@ GRAMMAR EXTEND Gram | IDENT "Grammar"; ent = IDENT -> (* This should be in "syntax" section but is here for factorization*) { PrintGrammar ent } + | IDENT "Custom"; IDENT "Grammar"; ent = IDENT -> + (* Should also be in "syntax" section *) + { PrintCustomGrammar ent } | IDENT "LoadPath"; dir = OPT dirpath -> { PrintLoadPath dir } | IDENT "Modules" -> { user_err Pp.(str "Print Modules is obsolete; use Print Libraries instead") } diff --git a/vernac/himsg.ml b/vernac/himsg.ml index f58eeae6dc..b2382ce6fc 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1348,9 +1348,6 @@ let explain_pattern_matching_error env sigma = function | CannotInferPredicate typs -> explain_cannot_infer_predicate env sigma typs -let map_pguard_error = map_pguard_error -let map_ptype_error = map_ptype_error - let explain_reduction_tactic_error = function | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) -> let e = map_ptype_error EConstr.of_constr e in diff --git a/vernac/himsg.mli b/vernac/himsg.mli index d0f42ea16b..d1c1c092e3 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -43,9 +43,4 @@ val explain_module_error : Modops.module_typing_error -> Pp.t val explain_module_internalization_error : Modintern.module_internalization_error -> Pp.t -val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error -[@@ocaml.deprecated "Use [Type_errors.map_pguard_error]."] -val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error -[@@ocaml.deprecated "Use [Type_errors.map_ptype_error]."] - val explain_prim_token_notation_error : string -> env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 843296d24e..50914959dc 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -50,10 +50,10 @@ let pr_entry e = str (Buffer.contents entry_buf) let pr_registered_grammar name = - let gram = try Some (Pcoq.find_grammars_by_name name) with Not_found -> None in + let gram = Pcoq.find_grammars_by_name name in match gram with - | None -> user_err Pp.(str "Unknown or unprintable grammar entry.") - | Some entries -> + | [] -> user_err Pp.(str "Unknown or unprintable grammar entry.") + | entries -> let pr_one (Pcoq.AnyEntry e) = str "Entry " ++ str (Pcoq.Entry.name e) ++ str " is" ++ fnl () ++ pr_entry e @@ -85,6 +85,8 @@ let pr_grammar = function pr_entry Pvernac.Vernac_.gallina_ext | name -> pr_registered_grammar name +let pr_custom_grammar name = pr_registered_grammar ("constr:"^name) + (**********************************************************************) (* Parse a format (every terminal starting with a letter or a single quote (except a single quote alone) must be quoted) *) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 38dbdf7e41..6435df23c7 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -57,6 +57,7 @@ val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr -> (** Print the Camlp5 state of a grammar *) val pr_grammar : string -> Pp.t +val pr_custom_grammar : string -> Pp.t val check_infix_modifiers : syntax_modifier list -> unit diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 889dbafabd..f2332bab8b 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -476,6 +476,8 @@ open Pputils keyword "Print Section" ++ spc() ++ Libnames.pr_qualid s | PrintGrammar ent -> keyword "Print Grammar" ++ spc() ++ str ent + | PrintCustomGrammar ent -> + keyword "Print Custom Grammar" ++ spc() ++ str ent | PrintLoadPath dir -> keyword "Print LoadPath" ++ pr_opt DirPath.print dir | PrintModules -> diff --git a/vernac/record.ml b/vernac/record.ml index f489707eb3..f737a8c524 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -276,8 +276,13 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields = let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in Termops.substl_rel_context (subst @ subst') fields +type projection_flags = { + pf_subclass: bool; + pf_canonical: bool; +} + (* We build projections *) -let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers fieldimpls fields = +let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in @@ -299,7 +304,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f in let (_,_,kinds,sp_projs,_) = List.fold_left3 - (fun (nfi,i,kinds,sp_projs,subst) coe decl impls -> + (fun (nfi,i,kinds,sp_projs,subst) flags decl impls -> let fi = RelDecl.get_name decl in let ti = RelDecl.get_type decl in let (sp_projs,i,subst) = @@ -359,17 +364,17 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f in let refi = ConstRef kn in Impargs.maybe_declare_manual_implicits false refi impls; - if coe then begin + if flags.pf_subclass then begin let cl = Class.class_of_global (IndRef indsp) in Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl end; let i = if is_local_assum decl then i+1 else i in (Some kn::sp_projs, i, Projection term::subst) with NotDefinable why -> - warning_or_error coe indsp why; + warning_or_error flags.pf_subclass indsp why; (None::sp_projs,i,NoProjection fi::subst) in - (nfi-1,i,(fi, is_local_assum decl)::kinds,sp_projs,subst)) - (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls) + (nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst)) + (List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls) in (kinds,sp_projs) open Typeclasses @@ -525,7 +530,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity in [cref, [Name proj_name, sub, Some proj_cst]] | _ -> - let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in + let record_data = [id, idbuild, arity, fieldimpls, fields, false, + List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls params template ~kind:Method ~name:[|binder_name|] record_data in @@ -699,7 +705,11 @@ let definition_structure udecl kind ~template cum poly finite records = let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = - let coe = List.map (fun (_, { rf_subclass }) -> not (Option.is_empty rf_subclass)) cfs in + let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) -> + { pf_subclass = not (Option.is_empty rf_subclass); + pf_canonical = rf_canonical }) + cfs + in id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe in let data = List.map2 map data records in diff --git a/vernac/record.mli b/vernac/record.mli index d6e63901cd..24bb27e107 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -14,15 +14,20 @@ open Constrexpr val primitive_flag : bool ref +type projection_flags = { + pf_subclass: bool; + pf_canonical: bool; +} + val declare_projections : inductive -> Entries.universes_entry -> ?kind:Decl_kinds.definition_object_kind -> Id.t -> - bool list -> + projection_flags list -> Impargs.manual_implicits list -> Constr.rel_context -> - (Name.t * bool) list * Constant.t option list + Recordops.proj_kind list * Constant.t option list val declare_structure_entry : Recordops.struc_tuple -> unit diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 279d4f0935..e1d134f3a9 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -744,7 +744,7 @@ let vernac_inductive ~atts cum lo finite indl = let (coe, (lid, ce)) = l in let coe' = if coe then Some true else None in let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce), - { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] } in + { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]] else if List.for_all is_record indl then (* Mutual record case *) @@ -1885,6 +1885,7 @@ let vernac_print ~(pstate : Proof_global.t option) ~atts = | PrintSectionContext qid -> print_sec_context_typ env sigma qid | PrintInspect n -> inspect env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent + | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir | PrintModules -> print_modules () | PrintModule qid -> print_module qid diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 34a9b9394a..23633e39ab 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -29,6 +29,7 @@ type printable = | PrintSectionContext of qualid | PrintInspect of int | PrintGrammar of string + | PrintCustomGrammar of string | PrintLoadPath of DirPath.t option | PrintModules | PrintModule of qualid @@ -148,6 +149,7 @@ type record_field_attr = { rf_subclass: instance_flag; (* the projection is an implicit coercion or an instance *) rf_priority: int option; (* priority of the instance, if relevant *) rf_notation: decl_notation list; + rf_canonical: bool; (* use this projection in the search for canonical instances *) } type constructor_expr = (lident * constr_expr) with_coercion type constructor_list_or_record_decl_expr = |