diff options
178 files changed, 1212 insertions, 1066 deletions
diff --git a/checker/check.ml b/checker/check.ml index a2c8a0f25d..76f40dbac2 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -50,7 +50,7 @@ let pr_path sp = type compilation_unit_name = DirPath.t -type seg_proofs = Constr.constr Future.computation array +type seg_proofs = Constr.constr option array type library_t = { library_name : compilation_unit_name; @@ -100,16 +100,7 @@ let access_opaque_table dp i = assert (i < Array.length t); t.(i) -let access_opaque_univ_table dp i = - try - let t = LibraryMap.find dp !opaque_univ_tables in - assert (i < Array.length t); - Some t.(i) - with Not_found -> None - -let () = - Opaqueproof.set_indirect_opaque_accessor access_opaque_table; - Opaqueproof.set_indirect_univ_accessor access_opaque_univ_table +let () = Mod_checking.set_indirect_accessor access_opaque_table let check_one_lib admit senv (dir,m) = let md = m.library_compiled in diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 1dd16f1630..1cf07e7cc7 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -8,6 +8,14 @@ open Environ (** {6 Checking constants } *) +let get_proof = ref (fun _ _ -> assert false) +let set_indirect_accessor f = get_proof := f + +let indirect_accessor = { + Opaqueproof.access_proof = (fun dp n -> !get_proof dp n); + Opaqueproof.access_constraints = (fun _ _ -> assert false); +} + let check_constant_declaration env kn cb = Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn); (* Locally set the oracle for further typechecking *) @@ -29,10 +37,16 @@ let check_constant_declaration env kn cb = in let ty = cb.const_type in let _ = infer_type env' ty in + let otab = Environ.opaque_tables env in + let body = match cb.const_body with + | Undef _ | Primitive _ -> None + | Def c -> Some (Mod_subst.force_constr c) + | OpaqueDef o -> Some (Opaqueproof.force_proof indirect_accessor otab o) + in let () = - match Environ.body_of_constant_body env cb with + match body with | Some bd -> - let j = infer env' (fst bd) in + let j = infer env' bd in (try conv_leq env' j.uj_type ty with NotConvertible -> Type_errors.error_actual_type env j ty) | None -> () diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli index 6cff3e6b8c..dbc81c8507 100644 --- a/checker/mod_checking.mli +++ b/checker/mod_checking.mli @@ -8,4 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +val set_indirect_accessor : (Names.DirPath.t -> int -> Constr.t option) -> unit + val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit diff --git a/checker/values.ml b/checker/values.ml index 5cbf0ff298..4b651cafb6 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -53,7 +53,6 @@ let v_enum name n = Sum(name,n,[||]) let v_pair v1 v2 = v_tuple "*" [|v1; v2|] let v_bool = v_enum "bool" 2 let v_unit = v_enum "unit" 1 -let v_ref v = v_tuple "ref" [|v|] let v_set v = let rec s = Sum ("Set.t",1, @@ -70,13 +69,6 @@ let v_hmap vk vd = v_map Int (v_map vk vd) let v_pred v = v_pair v_bool (v_set v) -(* lib/future *) -let v_computation f = - Annot ("Future.computation", - v_ref - (v_sum "Future.comput" 0 - [| [| Fail "Future.ongoing" |]; [| f |] |])) - (** kernel/names *) let v_id = String @@ -391,6 +383,6 @@ let v_libsum = let v_lib = Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) -let v_opaques = Array (v_computation v_constr) +let v_opaques = Array (Opt v_constr) let v_univopaques = - Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|])) + Opt (Tuple ("univopaques",[|Array (Opt v_context_set);v_context_set;v_bool|])) diff --git a/dev/build/windows/ReadMe.txt b/dev/build/windows/ReadMe.txt index 55b46c616c..052014824f 100644 --- a/dev/build/windows/ReadMe.txt +++ b/dev/build/windows/ReadMe.txt @@ -131,7 +131,7 @@ mingwinCygwin: Install coq in the default Cygwin mingw sysroot folder. Todo: The coq share folder should be configured to e.g. /share/coq. As is, coqc scans the complete share folder, which slows it down 5x for short files. -absoloute: Install coq in the absolute path given with -destcoq. +absolute: Install coq in the absolute path given with -destcoq. The resulting Coq will not be relocatable. That is the root folder must not be renamed/moved. @@ -299,7 +299,7 @@ The version of Coq to download and compile. Possible values: 8.4pl6, 8.5pl2, 8.5pl3, 8.6 (download from https://coq.inria.fr/distrib/V$COQ_VERSION/files/coq-<version>.tar.gz) Others versions might work, but are untested. - 8.4 is only tested in mode=absoloute + 8.4 is only tested in mode=absolute git-v8.6, git-trunk (download from https://github.com/coq/coq/archive/<version without git->.zip) diff --git a/dev/ci/user-overlays/09895-ejgallego-require+upper.sh b/dev/ci/user-overlays/09895-ejgallego-require+upper.sh new file mode 100644 index 0000000000..9a42c829ce --- /dev/null +++ b/dev/ci/user-overlays/09895-ejgallego-require+upper.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "9895" ] || [ "$CI_BRANCH" = "require+upper" ]; then + + quickchick_CI_REF=require+upper + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi diff --git a/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh b/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh new file mode 100644 index 0000000000..e3bbb84bcb --- /dev/null +++ b/dev/ci/user-overlays/10201-ppedrot-opaque-future-cleanup.sh @@ -0,0 +1,15 @@ +if [ "$CI_PULL_REQUEST" = "10201" ] || [ "$CI_BRANCH" = "opaque-future-cleanup" ]; then + + coq_dpdgraph_CI_REF=opaque-future-cleanup + coq_dpdgraph_CI_GITURL=https://github.com/ppedrot/coq-dpdgraph + + coqhammer_CI_REF=opaque-future-cleanup + coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer + + elpi_CI_REF=opaque-future-cleanup + elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi + + paramcoq_CI_REF=opaque-future-cleanup + paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq + +fi diff --git a/doc/changelog/02-specification-language/10167-orpat-mixfix.rst b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst new file mode 100644 index 0000000000..e3c3923348 --- /dev/null +++ b/doc/changelog/02-specification-language/10167-orpat-mixfix.rst @@ -0,0 +1,12 @@ +- Require parentheses around nested disjunctive patterns, so that pattern and + term syntax are consistent; match branch patterns no longer require + parentheses for notation at level 100 or more. Incompatibilities: + + + in :g:`match p with (_, (0|1)) => ...` parentheses may no longer be + omitted around :n:`0|1`. + + notation :g:`(p | q)` now potentially clashes with core pattern syntax, + and should be avoided. ``-w disj-pattern-notation`` flags such :cmd:`Notation`. + + see :ref:`extendedpatternmatching` for details + (`#10167 <https://github.com/coq/coq/pull/10167>`_, + by Georges Gonthier). diff --git a/doc/changelog/04-tactics/09288-injection-as.rst b/doc/changelog/04-tactics/09288-injection-as.rst new file mode 100644 index 0000000000..6a74551f06 --- /dev/null +++ b/doc/changelog/04-tactics/09288-injection-as.rst @@ -0,0 +1,4 @@ +- Documented syntax :n:`injection @term as [= {+ @intropattern} ]` as + an alternative to :n:`injection @term as {+ @simple_intropattern}` using + the standard :n:`@injection_intropattern` syntax (`#09288 + <https://github.com/coq/coq/pull/09288>`_, by Hugo Herbelin). diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml index cfc38ff9c9..22a0163fbb 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_print.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml @@ -11,7 +11,7 @@ let simple_body_access gref = failwith "constructors are not covered in this example" | Globnames.ConstRef cst -> let cb = Environ.lookup_constant cst (Global.env()) in - match Global.body_of_constant_body cb with + match Global.body_of_constant_body Library.indirect_accessor cb with | Some(e, _) -> e | None -> failwith "This term has no value" diff --git a/doc/sphinx/addendum/extended-pattern-matching.rst b/doc/sphinx/addendum/extended-pattern-matching.rst index e882ce6e88..b568160356 100644 --- a/doc/sphinx/addendum/extended-pattern-matching.rst +++ b/doc/sphinx/addendum/extended-pattern-matching.rst @@ -21,10 +21,10 @@ type is considered to be a variable. A variable name cannot occur more than once in a given pattern. It is recommended to start variable names by a lowercase letter. -If a pattern has the form ``(c x)`` where ``c`` is a constructor symbol and x +If a pattern has the form ``c x`` where ``c`` is a constructor symbol and x is a linear vector of (distinct) variables, it is called *simple*: it is the kind of pattern recognized by the basic version of match. On -the opposite, if it is a variable ``x`` or has the form ``(c p)`` with ``p`` not +the opposite, if it is a variable ``x`` or has the form ``c p`` with ``p`` not only made of variables, the pattern is called *nested*. A variable pattern matches any value, and the identifier is bound to @@ -216,7 +216,8 @@ Here is an example: end. -Here is another example using disjunctive subpatterns. +Nested disjunctive patterns are allowed, inside parentheses, with the +notation :n:`({+| @pattern})`, as in: .. coqtop:: in diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index 68f6d4008a..e58049b8d0 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -528,7 +528,7 @@ pass additional arguments such as ``using relation``. .. tacv:: setoid_reflexivity setoid_symmetry {? in @ident} setoid_transitivity - setoid_rewrite {? @orientation} @term {? at @occs} {? in @ident} + setoid_rewrite {? @orientation} @term {? at @occurrences} {? in @ident} setoid_replace @term with @term {? using relation @term} {? in @ident} {? by @tactic} :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; setoid_replace @@ -567,13 +567,13 @@ Printing relations and morphisms Deprecated syntax and backward incompatibilities ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Add Setoid @A @Aeq @ST as @ident +.. cmd:: Add Setoid @qualid__1 @qualid__2 @qualid__3 as @ident This command for declaring setoids and morphisms is also accepted due to backward compatibility reasons. - Here ``Aeq`` is a congruence relation without parameters, ``A`` is its carrier - and ``ST`` is an object of type (``Setoid_Theory A Aeq``) (i.e. a record + Here :n:`@qualid__2` is a congruence relation without parameters, :n:`@qualid__1` is its carrier + and :n:`@qualid__3` is an object of type (:n:`Setoid_Theory @qualid__1 @qualid__2`) (i.e. a record packing together the reflexivity, symmetry and transitivity lemmas). Notice that the syntax is not completely backward compatible since the identifier was not required. @@ -708,91 +708,65 @@ Definitions The generalized rewriting tactic is based on a set of strategies that can be combined to obtain custom rewriting procedures. Its set of strategies is based on Elan’s rewriting strategies :cite:`Luttik97specificationof`. Rewriting -strategies are applied using the tactic ``rewrite_strat s`` where ``s`` is a +strategies are applied using the tactic :n:`rewrite_strat @strategy` where :token:`strategy` is a strategy expression. Strategies are defined inductively as described by the following grammar: -.. productionlist:: rewriting - s, t, u : `strategy` - : `lemma` - : `lemma_right_to_left` - : `failure` - : `identity` - : `reflexivity` - : `progress` - : `failure_catch` - : `composition` - : `left_biased_choice` - : `iteration_one_or_more` - : `iteration_zero_or_more` - : `one_subterm` - : `all_subterms` - : `innermost_first` - : `outermost_first` - : `bottom_up` - : `top_down` - : `apply_hint` - : `any_of_the_terms` - : `apply_reduction` - : `fold_expression` - -.. productionlist:: rewriting - strategy : ( `s` ) - lemma : `c` - lemma_right_to_left : <- `c` - failure : fail - identity : id - reflexivity : refl - progress : progress `s` - failure_catch : try `s` - composition : `s` ; `u` - left_biased_choice : choice `s` `t` - iteration_one_or_more : repeat `s` - iteration_zero_or_more : any `s` - one_subterm : subterm `s` - all_subterms : subterms `s` - innermost_first : innermost `s` - outermost_first : outermost `s` - bottom_up : bottomup `s` - top_down : topdown `s` - apply_hint : hints `hintdb` - any_of_the_terms : terms (`c`)+ - apply_reduction : eval `redexpr` - fold_expression : fold `c` - +.. productionlist:: coq + strategy : `qualid` (lemma, left to right) + : <- `qualid` (lemma, right to left) + : fail (failure) + : id (identity) + : refl (reflexivity) + : progress `strategy` (progress) + : try `strategy` (try catch) + : `strategy` ; `strategy` (composition) + : choice `strategy` `strategy` (left_biased_choice) + : repeat `strategy` (one or more) + : any `strategy` (zero or more) + : subterm `strategy` (one subterm) + : subterms `strategy` (all subterms) + : innermost `strategy` (innermost first) + : outermost `strategy` (outermost first) + : bottomup `strategy` (bottom-up) + : topdown `strategy` (top-down) + : hints `ident` (apply hints from hint database) + : terms `term` ... `term` (any of the terms) + : eval `redexpr` (apply reduction) + : fold `term` (unify) + : ( `strategy` ) Actually a few of these are defined in term of the others using a primitive fixpoint operator: -.. productionlist:: rewriting - try `s` : choice `s` `id` - any `s` : fix `u`. try (`s` ; `u`) - repeat `s` : `s` ; any `s` - bottomup s : fix `bu`. (choice (progress (subterms bu)) s) ; try bu - topdown s : fix `td`. (choice s (progress (subterms td))) ; try td - innermost s : fix `i`. (choice (subterm i) s) - outermost s : fix `o`. (choice s (subterm o)) +- :n:`try @strategy := choice @strategy id` +- :n:`any @strategy := fix @ident. try (@strategy ; @ident)` +- :n:`repeat @strategy := @strategy; any @strategy` +- :n:`bottomup @strategy := fix @ident. (choice (progress (subterms @ident)) @strategy) ; try @ident` +- :n:`topdown @strategy := fix @ident. (choice @strategy (progress (subterms @ident))) ; try @ident` +- :n:`innermost @strategy := fix @ident. (choice (subterm @ident) @strategy)` +- :n:`outermost @strategy := fix @ident. (choice @strategy (subterm @ident))` The basic control strategy semantics are straightforward: strategies are applied to subterms of the term to rewrite, starting from the root of the term. The lemma strategies unify the left-hand-side of the lemma with the current subterm and on success rewrite it to the right- hand-side. Composition can be used to continue rewriting on the -current subterm. The fail strategy always fails while the identity +current subterm. The ``fail`` strategy always fails while the identity strategy succeeds without making progress. The reflexivity strategy succeeds, making progress using a reflexivity proof of rewriting. -Progress tests progress of the argument strategy and fails if no +``progress`` tests progress of the argument :token:`strategy` and fails if no progress was made, while ``try`` always succeeds, catching failures. -Choice is left-biased: it will launch the first strategy and fall back +``choice`` is left-biased: it will launch the first strategy and fall back on the second one in case of failure. One can iterate a strategy at least 1 time using ``repeat`` and at least 0 times using ``any``. -The ``subterm`` and ``subterms`` strategies apply their argument strategy ``s`` to +The ``subterm`` and ``subterms`` strategies apply their argument :token:`strategy` to respectively one or all subterms of the current term under consideration, left-to-right. ``subterm`` stops at the first subterm for -which ``s`` made progress. The composite strategies ``innermost`` and ``outermost`` +which :token:`strategy` made progress. The composite strategies ``innermost`` and ``outermost`` perform a single innermost or outermost rewrite using their argument -strategy. Their counterparts ``bottomup`` and ``topdown`` perform as many +:token:`strategy`. Their counterparts ``bottomup`` and ``topdown`` perform as many rewritings as possible, starting from the bottom or the top of the term. @@ -802,15 +776,15 @@ lemmas at the current subterm. The ``terms`` strategy takes the lemma names directly as arguments. The ``eval`` strategy expects a reduction expression (see :ref:`performingcomputations`) and succeeds if it reduces the subterm under consideration. The ``fold`` strategy takes -a term ``c`` and tries to *unify* it to the current subterm, converting it to ``c`` -on success, it is stronger than the tactic ``fold``. +a :token:`term` and tries to *unify* it to the current subterm, converting it to :token:`term` +on success. It is stronger than the tactic ``fold``. Usage ~~~~~ -.. tacn:: rewrite_strat @s {? in @ident } +.. tacn:: rewrite_strat @strategy {? in @ident } :name: rewrite_strat Rewrite using the strategy s in hypothesis ident or the conclusion. diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 3b350d5dc0..3f4d5cc784 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -310,10 +310,10 @@ The syntax for adding a new ring is .. productionlist:: coq ring_mod : abstract | decidable `term` | morphism `term` : setoid `term` `term` - : constants [`ltac`] - : preprocess [`ltac`] - : postprocess [`ltac`] - : power_tac `term` [`ltac`] + : constants [ `tactic` ] + : preprocess [ `tactic` ] + : postprocess [ `tactic` ] + : power_tac `term` [ `tactic` ] : sign `term` : div `term` @@ -341,31 +341,31 @@ The syntax for adding a new ring is This modifier needs not be used if the setoid and morphisms have been declared. - constants [ :n:`@ltac` ] - specifies a tactic expression :n:`@ltac` that, given a + constants [ :n:`@tactic` ] + specifies a tactic expression :n:`@tactic` that, given a term, returns either an object of the coefficient set that is mapped to the expression via the morphism, or returns ``InitialRing.NotConstant``. The default behavior is to map only 0 and 1 to their counterpart in the coefficient set. This is generally not desirable for non trivial computational rings. - preprocess [ :n:`@ltac` ] - specifies a tactic :n:`@ltac` that is applied as a + preprocess [ :n:`@tactic` ] + specifies a tactic :n:`@tactic` that is applied as a preliminary step for :tacn:`ring` and :tacn:`ring_simplify`. It can be used to transform a goal so that it is better recognized. For instance, ``S n`` can be changed to ``plus 1 n``. - postprocess [ :n:`@ltac` ] - specifies a tactic :n:`@ltac` that is applied as a final + postprocess [ :n:`@tactic` ] + specifies a tactic :n:`@tactic` that is applied as a final step for :tacn:`ring_simplify`. For instance, it can be used to undo modifications of the preprocessor. - power_tac :n:`@term` [ :n:`@ltac` ] + power_tac :n:`@term` [ :n:`@tactic` ] allows :tacn:`ring` and :tacn:`ring_simplify` to recognize power expressions with a constant positive integer exponent (example: :math:`x^2` ). The term :n:`@term` is a proof that a given power function satisfies the specification of a power function (term has to be a proof of - ``Ring_theory.power_theory``) and :n:`@ltac` specifies a tactic expression + ``Ring_theory.power_theory``) and :n:`@tactic` specifies a tactic expression that, given a term, “abstracts” it into an object of type |N| whose interpretation via ``Cp_phi`` (the evaluation function of power coefficient) is the original term, or returns ``InitialRing.NotConstant`` diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index 1aa2111816..395b5ce2d3 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -366,24 +366,32 @@ The syntax has been extended to allow users to explicitly bind names to universes and explicitly instantiate polymorphic definitions. .. cmd:: Universe @ident + Polymorphic Universe @ident In the monorphic case, this command declares a new global universe named :g:`ident`, which can be referred to using its qualified name as well. Global universe names live in a separate namespace. The - command supports the polymorphic flag only in sections, meaning the + command supports the ``Polymorphic`` flag only in sections, meaning the universe quantification will be discharged on each section definition independently. One cannot mix polymorphic and monomorphic declarations in the same section. -.. cmd:: Constraint @ident @ord @ident +.. cmd:: Constraint @universe_constraint + Polymorphic Constraint @universe_constraint - This command declares a new constraint between named universes. The - order relation :n:`@ord` can be one of :math:`<`, :math:`≤` or :math:`=`. If consistent, the constraint - is then enforced in the global environment. Like ``Universe``, it can be - used with the ``Polymorphic`` prefix in sections only to declare - constraints discharged at section closing time. One cannot declare a - global constraint on polymorphic universes. + This command declares a new constraint between named universes. + + .. productionlist:: coq + universe_constraint : `qualid` < `qualid` + : `qualid` <= `qualid` + : `qualid` = `qualid` + + If consistent, the constraint is then enforced in the global + environment. Like :cmd:`Universe`, it can be used with the + ``Polymorphic`` prefix in sections only to declare constraints + discharged at section closing time. One cannot declare a global + constraint on polymorphic universes. .. exn:: Undeclared universe @ident. :undocumented: diff --git a/doc/sphinx/conf.py b/doc/sphinx/conf.py index ec3343dac6..53309cd313 100755 --- a/doc/sphinx/conf.py +++ b/doc/sphinx/conf.py @@ -181,7 +181,21 @@ suppress_warnings = ["misc.highlighting_failure"] todo_include_todos = False # Extra warnings, including undefined references -nitpicky = False +nitpicky = True + +nitpick_ignore = [ ('token', token) for token in [ + 'tactic', + # 142 occurrences currently sort of defined in the ltac chapter, + # but is it the right place? + 'module', + 'redexpr', + 'modpath', + 'dirpath', + 'collection', + 'term_pattern', + 'term_pattern_string', + 'command', + 'symbol' ]] # -- Options for HTML output ---------------------------------------------- diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 2b673ff62b..c1af4d067f 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -603,11 +603,16 @@ The following experimental command is available when the ``FunInd`` library has The meaning of this declaration is to define a function ident, similarly to ``Fixpoint``. Like in ``Fixpoint``, the decreasing argument must be given (unless the function is not recursive), but it might not - necessarily be *structurally* decreasing. The point of the {} annotation + necessarily be *structurally* decreasing. The point of the :n:`{ @decrease_annot }` annotation is to name the decreasing argument *and* to describe which kind of decreasing criteria must be used to ensure termination of recursive calls. + .. productionlist:: + decrease_annot : struct `ident` + : measure `term` `ident` + : wf `term` `ident` + The ``Function`` construction also enjoys the ``with`` extension to define mutually recursive definitions. However, this feature does not work for non structurally recursive functions. @@ -616,31 +621,33 @@ See the documentation of functional induction (:tacn:`function induction`) and ``Functional Scheme`` (:ref:`functional-scheme`) for how to use the induction principle to easily reason about the function. -Remark: To obtain the right principle, it is better to put rigid -parameters of the function as first arguments. For example it is -better to define plus like this: +.. note:: -.. coqtop:: reset none + To obtain the right principle, it is better to put rigid + parameters of the function as first arguments. For example it is + better to define plus like this: - Require Import FunInd. + .. coqtop:: reset none -.. coqtop:: all + Require Import FunInd. - Function plus (m n : nat) {struct n} : nat := - match n with - | 0 => m - | S p => S (plus m p) - end. + .. coqtop:: all -than like this: + Function plus (m n : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus m p) + end. -.. coqtop:: reset all + than like this: - Function plus (n m : nat) {struct n} : nat := - match n with - | 0 => m - | S p => S (plus p m) - end. + .. coqtop:: reset all + + Function plus (n m : nat) {struct n} : nat := + match n with + | 0 => m + | S p => S (plus p m) + end. *Limitations* @@ -710,7 +717,7 @@ used by ``Function``. A more precise description is given below. with :cmd:`Fixpoint`. Moreover the following are defined: + The same objects as above; - + The fixpoint equation of :token:`ident`: :n:`@ident_equation`. + + The fixpoint equation of :token:`ident`: :token:`ident`\ ``_equation``. .. cmdv:: Function @ident {* @binder } { measure @term @ident } : @type := @term Function @ident {* @binder } { wf @term @ident } : @type := @term @@ -1909,7 +1916,7 @@ This syntax extension is given in the following grammar: Renaming implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~ -.. cmd:: Arguments @qualid {* @name} : @rename +.. cmd:: Arguments @qualid {* @name} : rename :name: Arguments (rename) This command is used to redefine the names of implicit arguments. @@ -2296,7 +2303,7 @@ Printing universes language, and can be processed by Graphviz tools. The format is unspecified if `string` doesn’t end in ``.dot`` or ``.gv``. -.. cmdv:: Print Universes Subgraph(@names) +.. cmdv:: Print Universes Subgraph({+ @qualid }) :name: Print Universes Subgraph Prints the graph restricted to the requested names (adjusting diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index 8acbcbec8f..ebaa6fde66 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -185,8 +185,7 @@ is described in Chapter :ref:`syntaxextensionsandinterpretationscopes`. : `qualid` : _ : `num` - : ( `or_pattern` , … , `or_pattern` ) - or_pattern : `pattern` | … | `pattern` + : ( `pattern` | … | `pattern` ) Types diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 0a95a6edd6..c48dd5b99e 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -32,22 +32,25 @@ The syntax of the tactic language is given below. See Chapter :ref:`gallinaspecificationlanguage` for a description of the BNF metasyntax used in these grammar rules. Various already defined entries will be used in this chapter: entries :token:`natural`, :token:`integer`, :token:`ident`, -:token:`qualid`, :token:`term`, :token:`cpattern` and :token:`atomic_tactic` +:token:`qualid`, :token:`term`, :token:`cpattern` and :token:`tactic` represent respectively the natural and integer numbers, the authorized identificators and qualified names, Coq terms and patterns and all the atomic -tactics described in Chapter :ref:`tactics`. The syntax of :token:`cpattern` is +tactics described in Chapter :ref:`tactics`. + +The syntax of :production:`cpattern` is the same as that of terms, but it is extended with pattern matching metavariables. In :token:`cpattern`, a pattern matching metavariable is -represented with the syntax :g:`?id` where :g:`id` is an :token:`ident`. The +represented with the syntax :n:`?@ident`. The notation :g:`_` can also be used to denote metavariable whose instance is -irrelevant. In the notation :g:`?id`, the identifier allows us to keep +irrelevant. In the notation :n:`?@ident`, the identifier allows us to keep instantiations and to make constraints whereas :g:`_` shows that we are not interested in what will be matched. On the right hand side of pattern matching clauses, the named metavariables are used without the question mark prefix. There is also a special notation for second-order pattern matching problems: in an -applicative pattern of the form :g:`@?id id1 … idn`, the variable id matches any -complex expression with (possible) dependencies in the variables :g:`id1 … idn` -and returns a functional term of the form :g:`fun id1 … idn => term`. +applicative pattern of the form :n:`%@?@ident @ident__1 … @ident__n`, +the variable :token:`ident` matches any complex expression with (possible) +dependencies in the variables :n:`@ident__i` and returns a functional term +of the form :n:`fun @ident__1 … ident__n => @term`. The main entry of the grammar is :n:`@expr`. This language is used in proof mode but it can also be used in toplevel definitions as shown below. @@ -133,7 +136,7 @@ mode but it can also be used in toplevel definitions as shown below. : guard `test` : assert_fails `tacexpr3` : assert_succeeds `tacexpr3` - : `atomic_tactic` + : `tactic` : `qualid` `tacarg` ... `tacarg` : `atom` atom : `qualid` diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index aa603fc966..5f2e911ff9 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -124,13 +124,13 @@ Type declarations One can define new types by the following commands. -.. cmd:: Ltac2 Type @ltac2_typeparams @lident +.. cmd:: Ltac2 Type {? @ltac2_typeparams } @lident :name: Ltac2 Type This command defines an abstract type. It has no use for the end user and is dedicated to types representing data coming from the OCaml world. -.. cmdv:: Ltac2 Type {? rec} @ltac2_typeparams @lident := @ltac2_typedef +.. cmdv:: Ltac2 Type {? rec} {? @ltac2_typeparams } @lident := @ltac2_typedef This command defines a type with a manifest. There are four possible kinds of such definitions: alias, variant, record and open variant types. @@ -154,7 +154,7 @@ One can define new types by the following commands. Records are product types with named fields and eliminated by projection. Likewise they can be recursive if the `rec` flag is set. - .. cmdv:: Ltac2 Type @ltac2_typeparams @ltac2_qualid := [ @ltac2_constructordef ] + .. cmdv:: Ltac2 Type {? @ltac2_typeparams } @ltac2_qualid ::= [ @ltac2_constructordef ] Open variants are a special kind of variant types whose constructors are not statically defined, but can instead be extended dynamically. A typical example @@ -179,7 +179,7 @@ constructions from ML. : let `ltac2_var` := `ltac2_term` in `ltac2_term` : let rec `ltac2_var` := `ltac2_term` in `ltac2_term` : match `ltac2_term` with `ltac2_branch` ... `ltac2_branch` end - : `int` + : `integer` : `string` : `ltac2_term` ; `ltac2_term` : [| `ltac2_term` ; ... ; `ltac2_term` |] @@ -619,7 +619,7 @@ calls to term matching functions from the `Pattern` module. Internally, it is implemented thanks to a specific scope accepting the :n:`@constrmatching` syntax. Variables from the :n:`@constrpattern` are statically bound in the body of the branch, to -values of type `constr` for the variables from the :n:`@constr` pattern and to a +values of type `constr` for the variables from the :n:`@term` pattern and to a value of type `Pattern.context` for the variable :n:`@lident`. Note that unlike Ltac, only lowercase identifiers are valid as Ltac2 @@ -686,20 +686,22 @@ The following scopes are built-in. - :n:`list0(@ltac2_scope)`: - + if :n:`@ltac2_scope` parses :production:`entry`, parses :n:`(@entry__0, ..., @entry__n)` and produces - :n:`[@entry__0; ...; @entry__n]`. + + if :n:`@ltac2_scope` parses :n:`@quotentry`, + then it parses :n:`(@quotentry__0, ..., @quotentry__n)` and produces + :n:`[@quotentry__0; ...; @quotentry__n]`. - :n:`list0(@ltac2_scope, sep = @string__sep)`: - + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`(@entry__0 @string__sep ... @string__sep @entry__n)` - and produces :n:`[@entry__0; ...; @entry__n]`. + + if :n:`@ltac2_scope` parses :n:`@quotentry`, + then it parses :n:`(@quotentry__0 @string__sep ... @string__sep @quotentry__n)` + and produce :n:`[@quotentry__0; ...; @quotentry__n]`. -- :n:`list1`: same as :n:`list0` (with or without separator) but parses :n:`{+ @entry}` instead - of :n:`{* @entry}`. +- :n:`list1`: same as :n:`list0` (with or without separator) but parses :n:`{+ @quotentry}` instead + of :n:`{* @quotentry}`. - :n:`opt(@ltac2_scope)` - + if :n:`@ltac2_scope` parses :n:`@entry`, parses :n:`{? @entry}` and produces either :n:`None` or + + if :n:`@ltac2_scope` parses :n:`@quotentry`, parses :n:`{? @quotentry}` and produces either :n:`None` or :n:`Some x` where :n:`x` is the parsed expression. - :n:`self`: diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 4a2f9c0db3..3f966755ca 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -175,12 +175,12 @@ list of assertion commands is given in :ref:`Assertions`. The command Use all section variables except the list of :token:`ident`. - .. cmdv:: Proof using @collection1 + @collection2 + .. cmdv:: Proof using @collection__1 + @collection__2 Use section variables from the union of both collections. See :ref:`nameaset` to know how to form a named collection. - .. cmdv:: Proof using @collection1 - @collection2 + .. cmdv:: Proof using @collection__1 - @collection__2 Use section variables which are in the first collection but not in the second one. @@ -202,10 +202,10 @@ Proof using options The following options modify the behavior of ``Proof using``. -.. opt:: Default Proof Using "@expression" +.. opt:: Default Proof Using "@collection" :name: Default Proof Using - Use :n:`@expression` as the default ``Proof using`` value. E.g. ``Set Default + Use :n:`@collection` as the default ``Proof using`` value. E.g. ``Set Default Proof Using "a b"`` will complete all ``Proof`` commands not followed by a ``using`` part with ``using a b``. @@ -220,7 +220,7 @@ The following options modify the behavior of ``Proof using``. Name a set of section hypotheses for ``Proof using`` ```````````````````````````````````````````````````` -.. cmd:: Collection @ident := @expression +.. cmd:: Collection @ident := @collection This can be used to name a set of section hypotheses, with the purpose of making ``Proof using`` annotations more diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 4002d157d3..cc4976587d 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -3478,7 +3478,7 @@ efficient ones, e.g. for the purpose of a correctness proof. Wildcards vs abstractions ````````````````````````` -The rewrite tactic supports :token:`r_items` containing holes. For example, in +The rewrite tactic supports :token:`r_item`\s containing holes. For example, in the tactic ``rewrite (_ : _ * 0 = 0).`` the term ``_ * 0 = 0`` is interpreted as ``forall n : nat, n * 0 = 0.`` Anyway this tactic is *not* equivalent to @@ -3753,7 +3753,7 @@ involves the following steps: 3. If so :tacn:`under` puts these n goals in head normal form (using the defective form of the tactic :tacn:`move`), then executes - the corresponding intro pattern :n:`@ipat__i` in each goal. + the corresponding intro pattern :n:`@i_pattern__i` in each goal. 4. Then :tacn:`under` checks that the first n subgoals are (quantified) equalities or double implications between a @@ -3802,11 +3802,11 @@ One-liner mode The Ltac expression: -:n:`under @term => [ @i_item__1 | … | @i_item__n ] do [ @tac__1 | … | @tac__n ].` +:n:`under @term => [ @i_item__1 | … | @i_item__n ] do [ @tactic__1 | … | @tactic__n ].` can be seen as a shorter form for the following expression: -:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tac__1; over | … | @tac__n; over | cbv beta iota ].` +:n:`(under @term) => [ @i_item__1 | … | @i_item__n | ]; [ @tactic__1; over | … | @tactic__n; over | cbv beta iota ].` Notes: @@ -3819,14 +3819,14 @@ Notes: involving the `bigop` theory from the Mathematical Components library. + If there is only one tactic, the brackets can be omitted, e.g.: - :n:`under @term => i do @tac.` and that shorter form should be + :n:`under @term => i do @tactic.` and that shorter form should be preferred. + If the ``do`` clause is provided and the intro pattern is omitted, then the default :token:`i_item` ``*`` is applied to each branch. E.g., the Ltac expression: - :n:`under @term do [ @tac__1 | … | @tac__n ]` is equivalent to: - :n:`under @term => [ * | … | * ] do [ @tac__1 | … | @tac__n ]` + :n:`under @term do [ @tactic__1 | … | @tactic__n ]` is equivalent to: + :n:`under @term => [ * | … | * ] do [ @tactic__1 | … | @tactic__n ]` (and it can be noted here that the :tacn:`under` tactic performs a ``move.`` before processing the intro patterns ``=> [ * | … | * ]``). @@ -4237,7 +4237,7 @@ selecting a specific redex and has been described in the previous sections. We have seen so far that the possibility of selecting a redex using a term with holes is already a powerful means of redex selection. Similarly, any terms provided by the user in the more -complex forms of :token:`c_patterns` +complex forms of :token:`c_pattern`\s presented in the tables above can contain holes. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index cdd23f4d06..fa6d62ffa2 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -131,16 +131,17 @@ include :tacn:`assert`, :tacn:`intros` and :tacn:`destruct`. simple_intropattern_closed : `naming_intropattern` : _ : `or_and_intropattern` - : `equality_intropattern` + : `rewriting_intropattern` + : `injection_intropattern` naming_intropattern : `ident` : ? : ?`ident` or_and_intropattern : [ `intropattern_list` | ... | `intropattern_list` ] : ( `simple_intropattern` , ... , `simple_intropattern` ) : ( `simple_intropattern` & ... & `simple_intropattern` ) - equality_intropattern : -> + rewriting_intropattern : -> : <- - : [= `intropattern_list` ] + injection_intropattern : [= `intropattern_list` ] or_and_intropattern_loc : `or_and_intropattern` : `ident` @@ -462,7 +463,7 @@ Occurrence sets and occurrence clauses An occurrence clause is a modifier to some tactics that obeys the following syntax: - .. productionlist:: sentence + .. productionlist:: coq occurrence_clause : in `goal_occurrences` goal_occurrences : [`ident` [`at_occurrences`], ... , `ident` [`at_occurrences`] [|- [* [`at_occurrences`]]]] : * |- [* [`at_occurrences`]] @@ -2127,7 +2128,7 @@ and an explanation of the underlying technique. :name: discriminate This tactic proves any goal from an assumption stating that two - structurally different :n:`@terms` of an inductive set are equal. For + structurally different :n:`@term`\s of an inductive set are equal. For example, from :g:`(S (S O))=(S O)` we can derive by absurdity any proposition. @@ -2285,6 +2286,18 @@ and an explanation of the underlying technique. to the number of new equalities. The original equality is erased if it corresponds to a hypothesis. + .. tacv:: injection @term {? with @bindings_list} as @injection_intropattern + injection @num as @injection_intropattern + injection as @injection_intropattern + einjection @term {? with @bindings_list} as @injection_intropattern + einjection @num as @injection_intropattern + einjection as @injection_intropattern + + These are equivalent to the previous variants but using instead the + syntax :token:`injection_intropattern` which :tacn:`intros` + uses. In particular :n:`as [= {+ @simple_intropattern}]` behaves + the same as :n:`as {+ @simple_intropattern}`. + .. flag:: Structural Injection This option ensure that :n:`injection @term` erases the original hypothesis @@ -2294,7 +2307,7 @@ and an explanation of the underlying technique. .. flag:: Keep Proof Equalities - By default, :tacn:`injection` only creates new equalities between :n:`@terms` + By default, :tacn:`injection` only creates new equalities between :n:`@term`\s whose type is in sort :g:`Type` or :g:`Set`, thus implementing a special behavior for objects that are proofs of a statement in :g:`Prop`. This option controls this behavior. @@ -2705,8 +2718,8 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacv:: rewrite @term in @goal_occurrences - Analogous to :n:`rewrite @term` but rewriting is done following clause - (similarly to :ref:`performing computations <performingcomputations>`). For instance: + Analogous to :n:`rewrite @term` but rewriting is done following + the clause :token:`goal_occurrences`. For instance: + :n:`rewrite H in H'` will rewrite `H` in the hypothesis ``H'`` instead of the current goal. @@ -2724,7 +2737,7 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. .. tacv:: rewrite @term at @occurrences - Rewrite only the given occurrences of :token:`term`. Occurrences are + Rewrite only the given :token:`occurrences` of :token:`term`. Occurrences are specified from left to right as for pattern (:tacn:`pattern`). The rewrite is always performed using setoid rewriting, even for Leibniz’s equality, so one has to ``Import Setoid`` to use this variant. @@ -2734,11 +2747,11 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. Use tactic to completely solve the side-conditions arising from the :tacn:`rewrite`. - .. tacv:: rewrite {+, @term} + .. tacv:: rewrite {+, @orientation @term} {? in @ident } Is equivalent to the `n` successive tactics :n:`{+; rewrite @term}`, each one - working on the first subgoal generated by the previous one. Orientation - :g:`->` or :g:`<-` can be inserted before each :token:`term` to rewrite. One + working on the first subgoal generated by the previous one. An :production:`orientation` + ``->`` or ``<-`` can be inserted before each :token:`term` to rewrite. One unique clause can be added at the end after the keyword in; it will then affect all rewrite operations. @@ -2799,12 +2812,12 @@ simply :g:`t=u` dropping the implicit type of :g:`t` and :g:`u`. Replaces :n:`@term` with :n:`@term’` using the first assumption whose type has the form :n:`@term’ = @term` - .. tacv:: replace @term {? with @term} in @goal_occurences {? by @tactic} - replace -> @term in @goal_occurences - replace <- @term in @goal_occurences + .. tacv:: replace @term {? with @term} in @goal_occurrences {? by @tactic} + replace -> @term in @goal_occurrences + replace <- @term in @goal_occurrences Acts as before but the replacements take place in the specified clauses - (:token:`goal_occurences`) (see :ref:`performingcomputations`) and not + (:token:`goal_occurrences`) (see :ref:`performingcomputations`) and not only in the conclusion of the goal. The clause argument must not contain any ``type of`` nor ``value of``. @@ -3065,7 +3078,7 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: native_compute :name: native_compute - This tactic evaluates the goal by compilation to Objective Caml as described + This tactic evaluates the goal by compilation to OCaml as described in :cite:`FullReduction`. If Coq is running in native code, it can be typically two to five times faster than ``vm_compute``. Note however that the compilation cost is higher, so it is worth using only for intensive @@ -3231,8 +3244,8 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: simpl @pattern - This applies ``simpl`` only to the subterms matching :n:`@pattern` in the - current goal. + This applies :tacn:`simpl` only to the subterms matching + :n:`@pattern` in the current goal. .. tacv:: simpl @pattern at {+ @num} @@ -3265,51 +3278,77 @@ the conversion in hypotheses :n:`{+ @ident}`. This tactic applies to any goal. The argument qualid must denote a defined transparent constant or local definition (see - :ref:`gallina-definitions` and :ref:`vernac-controlling-the-reduction-strategies`). The tactic - ``unfold`` applies the :math:`\delta` rule to each occurrence of the constant to which - :n:`@qualid` refers in the current goal and then replaces it with its - :math:`\beta`:math:`\iota`-normal form. + :ref:`gallina-definitions` and + :ref:`vernac-controlling-the-reduction-strategies`). The tactic + :tacn:`unfold` applies the :math:`\delta` rule to each occurrence of + the constant to which :n:`@qualid` refers in the current goal and + then replaces it with its :math:`\beta`:math:`\iota`-normal form. -.. exn:: @qualid does not denote an evaluable constant. - :undocumented: + .. exn:: @qualid does not denote an evaluable constant. + + This error is frequent when trying to unfold something that has + defined as an inductive type (or constructor) and not as a + definition. -.. tacv:: unfold @qualid in @ident + .. example:: - Replaces :n:`@qualid` in hypothesis :n:`@ident` with its definition - and replaces the hypothesis with its :math:`\beta`:math:`\iota` normal form. + .. coqtop:: abort all fail -.. tacv:: unfold {+, @qualid} + Goal 0 <= 1. + unfold le. - Replaces *simultaneously* :n:`{+, @qualid}` with their definitions and - replaces the current goal with its :math:`\beta`:math:`\iota` normal form. + This error can also be raised if you are trying to unfold + something that has been marked as opaque. -.. tacv:: unfold {+, @qualid at {+, @num }} + .. example:: - The lists :n:`{+, @num}` specify the occurrences of :n:`@qualid` to be - unfolded. Occurrences are located from left to right. + .. coqtop:: abort all fail - .. exn:: Bad occurrence number of @qualid. - :undocumented: + Opaque Nat.add. + Goal 1 + 0 = 1. + unfold Nat.add. - .. exn:: @qualid does not occur. - :undocumented: + .. tacv:: unfold @qualid in @goal_occurrences + + Replaces :n:`@qualid` in hypothesis (or hypotheses) designated + by :token:`goal_occurrences` with its definition and replaces + the hypothesis with its :math:`\beta`:math:`\iota` normal form. -.. tacv:: unfold @string + .. tacv:: unfold {+, @qualid} - If :n:`@string` denotes the discriminating symbol of a notation (e.g. "+") or - an expression defining a notation (e.g. `"_ + _"`), and this notation refers to an unfoldable constant, then the - tactic unfolds it. + Replaces :n:`{+, @qualid}` with their definitions and replaces + the current goal with its :math:`\beta`:math:`\iota` normal + form. -.. tacv:: unfold @string%@ident + .. tacv:: unfold {+, @qualid at @occurrences } - This is variant of :n:`unfold @string` where :n:`@string` gets its - interpretation from the scope bound to the delimiting key :token:`ident` - instead of its default interpretation (see :ref:`Localinterpretationrulesfornotations`). + The list :token:`occurrences` specify the occurrences of + :n:`@qualid` to be unfolded. Occurrences are located from left + to right. -.. tacv:: unfold {+, @qualid_or_string at {+, @num}} + .. exn:: Bad occurrence number of @qualid. + :undocumented: + + .. exn:: @qualid does not occur. + :undocumented: + + .. tacv:: unfold @string + + If :n:`@string` denotes the discriminating symbol of a notation + (e.g. "+") or an expression defining a notation (e.g. `"_ + + _"`), and this notation denotes an application whose head symbol + is an unfoldable constant, then the tactic unfolds it. - This is the most general form, where :n:`qualid_or_string` is either a - :n:`@qualid` or a :n:`@string` referring to a notation. + .. tacv:: unfold @string%@ident + + This is variant of :n:`unfold @string` where :n:`@string` gets + its interpretation from the scope bound to the delimiting key + :token:`ident` instead of its default interpretation (see + :ref:`Localinterpretationrulesfornotations`). + + .. tacv:: unfold {+, {| @qualid | @string{? %@ident } } {? at @occurrences } } {? in @goal_occurrences } + + This is the most general form. .. tacn:: fold @term :name: fold @@ -3448,9 +3487,9 @@ Automation :ref:`The Hints Databases for auto and eauto <thehintsdatabasesforautoandeauto>` for the list of pre-defined databases and the way to create or extend a database. - .. tacv:: auto using {+ @ident__i} {? with {+ @ident } } + .. tacv:: auto using {+ @qualid__i} {? with {+ @ident } } - Uses lemmas :n:`@ident__i` in addition to hints. If :n:`@ident` is an + Uses lemmas :n:`@qualid__i` in addition to hints. If :n:`@qualid` is an inductive type, it is the collection of its constructors which are added as hints. @@ -3458,8 +3497,8 @@ Automation The hints passed through the `using` clause are used in the same way as if they were passed through a hint database. Consequently, - they use a weaker version of :tacn:`apply` and :n:`auto using @ident` - may fail where :n:`apply @ident` succeeds. + they use a weaker version of :tacn:`apply` and :n:`auto using @qualid` + may fail where :n:`apply @qualid` succeeds. Given that this can be seen as counter-intuitive, it could be useful to have an option to use full-blown :tacn:`apply` for lemmas passed @@ -3477,7 +3516,7 @@ Automation Behaves like :tacn:`auto` but shows the tactics it tries to solve the goal, including failing paths. - .. tacv:: {? info_}auto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}auto {? @num} {? using {+ @qualid}} {? with {+ @ident}} This is the most general form, combining the various options. @@ -3490,10 +3529,10 @@ Automation .. tacv:: trivial with {+ @ident} trivial with * - trivial using {+ @lemma} + trivial using {+ @qualid} debug trivial info_trivial - {? info_}trivial {? using {+ @lemma}} {? with {+ @ident}} + {? info_}trivial {? using {+ @qualid}} {? with {+ @ident}} :name: _; _; _; debug trivial; info_trivial; _ :undocumented: @@ -3532,7 +3571,7 @@ Automation Note that ``ex_intro`` should be declared as a hint. - .. tacv:: {? info_}eauto {? @num} {? using {+ @lemma}} {? with {+ @ident}} + .. tacv:: {? info_}eauto {? @num} {? using {+ @qualid}} {? with {+ @ident}} The various options for :tacn:`eauto` are the same as for :tacn:`auto`. @@ -3551,9 +3590,9 @@ Automation This tactic unfolds constants that were declared through a :cmd:`Hint Unfold` in the given databases. -.. tacv:: autounfold with {+ @ident} in @goal_occurences +.. tacv:: autounfold with {+ @ident} in @goal_occurrences - Performs the unfolding in the given clause (:token:`goal_occurences`). + Performs the unfolding in the given clause (:token:`goal_occurrences`). .. tacv:: autounfold with * @@ -3593,10 +3632,9 @@ Automation Performs all the rewritings in hypothesis :n:`@qualid` applying :n:`@tactic` to the main subgoal after each rewriting step. -.. tacv:: autorewrite with {+ @ident} in @clause +.. tacv:: autorewrite with {+ @ident} in @goal_occurrences - Performs all the rewriting in the clause :n:`@clause`. The clause argument - must not contain any ``type of`` nor ``value of``. + Performs all the rewriting in the clause :n:`@goal_occurrences`. .. seealso:: @@ -3667,10 +3705,11 @@ automatically created. from the order in which they were inserted, making this implementation observationally different from the legacy one. -The general command to add a hint to some databases :n:`{+ @ident}` is - .. cmd:: Hint @hint_definition : {+ @ident} + The general command to add a hint to some databases :n:`{+ @ident}`. + The various possible :production:`hint_definition`\s are given below. + .. cmdv:: Hint @hint_definition No database name is given: the hint is registered in the ``core`` database. @@ -3719,7 +3758,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is before, the tactic actually used is a restricted version of :tacn:`apply`). - .. cmdv:: Resolve <- @term + .. cmdv:: Hint Resolve <- @term Adds the right-to-left implication of an equivalence as a hint. @@ -3739,7 +3778,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. exn:: @term cannot be used as a hint :undocumented: - .. cmdv:: Immediate {+ @term} : @ident + .. cmdv:: Hint Immediate {+ @term} : @ident Adds each :n:`Hint Immediate @term`. @@ -4557,14 +4596,14 @@ Automating .. _btauto_grammar: .. productionlist:: sentence - t : `x` - : true - : false - : orb `t` `t` - : andb `t` `t` - : xorb `t` `t` - : negb `t` - : if `t` then `t` else `t` + btauto_term : `ident` + : true + : false + : orb `btauto_term` `btauto_term` + : andb `btauto_term` `btauto_term` + : xorb `btauto_term` `btauto_term` + : negb `btauto_term` + : if `btauto_term` then `btauto_term` else `btauto_term` Whenever the formula supplied is not a tautology, it also provides a counter-example. diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index ffa727ff6c..5f3e82938d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -189,18 +189,13 @@ Requests to the environment This command displays the type of :n:`@term`. When called in proof mode, the term is checked in the local context of the current subgoal. - - .. TODO : selector is not a syntax entry - .. cmdv:: @selector: Check @term This variant specifies on which subgoal to perform typing (see Section :ref:`invocation-of-tactics`). -.. TODO : convtactic is not a syntax entry - -.. cmd:: Eval @convtactic in @term +.. cmd:: Eval @redexpr in @term This command performs the specified reduction on :n:`@term`, and displays the resulting term with its type. The term to be reduced may depend on @@ -1132,6 +1127,8 @@ described first. with lower level is expanded first. In case of a tie, the second one (appearing in the cast type) is expanded. + .. prodn:: level ::= {| opaque | @num | expand } + Levels can be one of the following (higher to lower): + ``opaque`` : level of opaque constants. They cannot be expanded by @@ -1167,19 +1164,19 @@ described first. Print all the currently non-transparent strategies. -.. cmd:: Declare Reduction @ident := @convtactic +.. cmd:: Declare Reduction @ident := @redexpr This command allows giving a short name to a reduction expression, for - instance lazy beta delta [foo bar]. This short name can then be used + instance ``lazy beta delta [foo bar]``. This short name can then be used in :n:`Eval @ident in` or ``eval`` directives. This command accepts the - Local modifier, for discarding this reduction name at the end of the - file or module. For the moment the name cannot be qualified. In + ``Local`` modifier, for discarding this reduction name at the end of the + file or module. For the moment, the name is not qualified. In particular declaring the same name in several modules or in several - functor applications will be refused if these declarations are not + functor applications will be rejected if these declarations are not local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but - nothing prevents the user to also perform a - :n:`Ltac @ident := @convtactic`. + nothing prevents the user from also performing a + :n:`Ltac @ident := @redexpr`. .. seealso:: :ref:`performingcomputations` diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 3710c0af9d..9b381cb9de 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -109,7 +109,7 @@ the associativity of disjunction and conjunction, so let us apply for instance a right associativity (which is the choice of Coq). Precedence levels and associativity rules of notations have to be -given between parentheses in a list of modifiers that the :cmd:`Notation` +given between parentheses in a list of :token:`modifiers` that the :cmd:`Notation` command understands. Here is how the previous examples refine. .. coqtop:: in @@ -249,7 +249,7 @@ bar of the notation. Check (sig (fun x : nat => x=x)). The second, more powerful control on printing is by using the format -modifier. Here is an example +:token:`modifier`. Here is an example .. coqtop:: all @@ -298,8 +298,8 @@ expression is performed at definition time. Type checking is done only at the time of use of the notation. .. note:: Sometimes, a notation is expected only for the parser. To do - so, the option ``only parsing`` is allowed in the list of modifiers - of :cmd:`Notation`. Conversely, the ``only printing`` modifier can be + so, the option ``only parsing`` is allowed in the list of :token:`modifiers` + of :cmd:`Notation`. Conversely, the ``only printing`` :token:`modifier` can be used to declare that a notation should only be used for printing and should not declare a parsing rule. In particular, such notations do not modify the parser. @@ -310,11 +310,11 @@ The Infix command The :cmd:`Infix` command is a shortening for declaring notations of infix symbols. -.. cmd:: Infix "@symbol" := @term ({+, @modifier}). +.. cmd:: Infix "@symbol" := @term {? (@modifiers) }. This command is equivalent to - :n:`Notation "x @symbol y" := (@term x y) ({+, @modifier}).` + :n:`Notation "x @symbol y" := (@term x y) {? (@modifiers) }.` where ``x`` and ``y`` are fresh names. Here is an example. @@ -437,7 +437,7 @@ application of the notation: Check sigma z : nat, z = 0. -Notice the modifier ``x ident`` in the declaration of the +Notice the :token:`modifier` ``x ident`` in the declaration of the notation. It tells to parse :g:`x` as a single identifier. Binders bound in the notation and parsed as patterns @@ -457,7 +457,7 @@ binder. Here is an example: Check subset '(x,y), x+y=0. -The modifier ``p pattern`` in the declaration of the notation tells to parse +The :token:`modifier` ``p pattern`` in the declaration of the notation tells to parse :g:`p` as a pattern. Note that a single variable is both an identifier and a pattern, so, e.g., the following also works: @@ -467,7 +467,7 @@ pattern, so, e.g., the following also works: If one wants to prevent such a notation to be used for printing when the pattern is reduced to a single identifier, one has to use instead -the modifier ``p strict pattern``. For parsing, however, a +the :token:`modifier` ``p strict pattern``. For parsing, however, a ``strict pattern`` will continue to include the case of a variable. Here is an example showing the difference: @@ -507,7 +507,7 @@ that ``x`` is parsed as a term at level 99 (as done in the notation for :g:`sumbool`), but that this term has actually to be an identifier. The notation :g:`{ x | P }` is already defined in the standard -library with the ``as ident`` modifier. We cannot redefine it but +library with the ``as ident`` :token:`modifier`. We cannot redefine it but one can define an alternative notation, say :g:`{ p such that P }`, using instead ``as pattern``. @@ -527,7 +527,7 @@ is just an identifier, one could have said ``p at level 99 as strict pattern``. Note also that in the absence of a ``as ident``, ``as strict pattern`` or -``as pattern`` modifiers, the default is to consider sub-expressions occurring +``as pattern`` :token:`modifier`\s, the default is to consider sub-expressions occurring in binding position and parsed as terms to be ``as ident``. .. _NotationsWithBinders: @@ -628,7 +628,7 @@ except that in the iterator position of the binding variable of a ``fun`` or a ``forall``. To specify that the part “``x .. y``” of the notation parses a sequence of -binders, ``x`` and ``y`` must be marked as ``binder`` in the list of modifiers +binders, ``x`` and ``y`` must be marked as ``binder`` in the list of :token:`modifiers` of the notation. The binders of the parsed sequence are used to fill the occurrences of the first placeholder of the iterating pattern which is repeatedly nested as many times as the number of binders generated. If ever the @@ -678,7 +678,7 @@ Predefined entries ~~~~~~~~~~~~~~~~~~ By default, sub-expressions are parsed as terms and the corresponding -grammar entry is called :n:`@constr`. However, one may sometimes want +grammar entry is called ``constr``. However, one may sometimes want to restrict the syntax of terms in a notation. For instance, the following notation will accept to parse only global reference in position of :g:`x`: @@ -866,16 +866,17 @@ notations are given below. The optional :production:`scope` is described in :ref:`Scopes`. .. productionlist:: coq - notation : [Local] Notation `string` := `term` [`modifiers`] [: `scope`]. - : [Local] Infix `string` := `qualid` [`modifiers`] [: `scope`]. - : [Local] Reserved Notation `string` [`modifiers`] . + notation : [Local] Notation `string` := `term` [(`modifiers`)] [: `scope`]. + : [Local] Infix `string` := `qualid` [(`modifiers`)] [: `scope`]. + : [Local] Reserved Notation `string` [(`modifiers`)] . : Inductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. : CoInductive `ind_body` [`decl_notation`] with … with `ind_body` [`decl_notation`]. : Fixpoint `fix_body` [`decl_notation`] with … with `fix_body` [`decl_notation`]. : CoFixpoint `cofix_body` [`decl_notation`] with … with `cofix_body` [`decl_notation`]. : [Local] Declare Custom Entry `ident`. decl_notation : [where `string` := `term` [: `scope`] and … and `string` := `term` [: `scope`]]. - modifiers : at level `num` + modifiers : `modifier`, … , `modifier` + modifier : at level `num` : in custom `ident` : in custom `ident` at level `num` : `ident` , … , `ident` at level `num` [`binderinterp`] @@ -924,6 +925,17 @@ notations are given below. The optional :production:`scope` is described in given to some notation, say ``"{ y } & { z }"`` in fact applies to the underlying ``"{ x }"``\-free rule which is ``"y & z"``). +.. note:: Notations such as ``"( p | q )"`` (or starting with ``"( x | "``, + more generally) are deprecated as they conflict with the syntax for + nested disjunctive patterns (see :ref:`extendedpatternmatching`), + and are not honored in pattern expressions. + + .. warn:: Use of @string Notation is deprecated as it is inconsistent with pattern syntax. + + This warning is disabled by default to avoid spurious diagnostics + due to legacy notation in the Coq standard library. + It can be turned on with the ``-w disj-pattern-notation`` flag. + Persistence of notations ++++++++++++++++++++++++ @@ -1141,10 +1153,10 @@ Binding types of arguments to an interpretation scope When an interpretation scope is naturally associated to a type (e.g. the scope of operations on the natural numbers), it may be convenient to bind it - to this type. When a scope ``scope`` is bound to a type ``type``, any new function - defined later on gets its arguments of type ``type`` interpreted by default in - scope ``scope`` (this default behavior can however be overwritten by explicitly - using the command :cmd:`Arguments <Arguments (scopes)>`). + to this type. When a scope :token:`scope` is bound to a type :token:`type`, any function + gets its arguments of type :token:`type` interpreted by default in scope :token:`scope` + (this default behavior can however be overwritten by explicitly using the + command :cmd:`Arguments <Arguments (scopes)>`). Whether the argument of a function has some type ``type`` is determined statically. For instance, if ``f`` is a polymorphic function of type @@ -1172,6 +1184,11 @@ Binding types of arguments to an interpretation scope Check (fun x y1 y2 z t => P _ (x + t) ((f _ (y1 + y2) + z))). + .. note:: When active, a bound scope has effect on all defined functions + (even if they are defined after the :cmd:`Bind Scope` directive), except + if argument scopes were assigned explicitly using the + :cmd:`Arguments <Arguments (scopes)>` command. + .. note:: The scopes ``type_scope`` and ``function_scope`` also have a local effect on interpretation. See the next section. @@ -1657,15 +1674,15 @@ Tactic notations allow to customize the syntax of tactics. They have the followi tacn : Tactic Notation [`tactic_level`] [`prod_item` … `prod_item`] := `tactic`. prod_item : `string` | `tactic_argument_type`(`ident`) tactic_level : (at level `num`) - tactic_argument_type : `ident` | `simple_intropattern` | `reference` - : `hyp` | `hyp_list` | `ne_hyp_list` - : `constr` | `uconstr` | `constr_list` | `ne_constr_list` - : `integer` | `integer_list` | `ne_integer_list` - : `int_or_var` | `int_or_var_list` | `ne_int_or_var_list` - : `tactic` | `tactic0` | `tactic1` | `tactic2` | `tactic3` - : `tactic4` | `tactic5` - -.. cmd:: Tactic Notation {? (at level @level)} {+ @prod_item} := @tactic. + tactic_argument_type : ident | simple_intropattern | reference + : hyp | hyp_list | ne_hyp_list + : constr | uconstr | constr_list | ne_constr_list + : integer | integer_list | ne_integer_list + : int_or_var | int_or_var_list | ne_int_or_var_list + : tactic | tactic0 | tactic1 | tactic2 | tactic3 + : tactic4 | tactic5 + +.. cmd:: Tactic Notation {? (at level @num)} {+ @prod_item} := @tactic. A tactic notation extends the parser and pretty-printer of tactics with a new rule made of the list of production items. It then evaluates into the diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 31f3736bae..1dd68f2abf 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1642,15 +1642,13 @@ let drop_notations_pattern looked_for genv = | CPatCast (_,_) -> (* We raise an error if the pattern contains a cast, due to current restrictions on casts in patterns. Cast in patterns - are supported only in local binders and only at top - level. In fact, they are currently eliminated by the - parser. The only reason why they are in the - [cases_pattern_expr] type is that the parser needs to factor - the "(c : t)" notation with user defined notations (such as - the pair). In the long term, we will try to support such - casts everywhere, and use them to print the domains of - lambdas in the encoding of match in constr. This check is - here and not in the parser because it would require + are supported only in local binders and only at top level. + The only reason they are in the [cases_pattern_expr] type + is that the parser needs to factor the "c : t" notation + with user defined notations. In the long term, we will try to + support such casts everywhere, and perhaps use them to print + the domains of lambdas in the encoding of match in constr. + This check is here and not in the parser because it would require duplicating the levels of the [pattern] rule. *) CErrors.user_err ?loc ~hdr:"drop_notations_pattern" (Pp.strbrk "Casts are not supported in this pattern.") diff --git a/kernel/environ.ml b/kernel/environ.ml index 05f342a82a..c47bde0864 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -483,16 +483,6 @@ let constant_value_and_type env (kn, u) = in b', subst_instance_constr u cb.const_type, cst -let body_of_constant_body env cb = - let otab = opaque_tables env in - match cb.const_body with - | Undef _ | Primitive _ -> - None - | Def c -> - Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb) - | OpaqueDef o -> - Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb) - (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) diff --git a/kernel/environ.mli b/kernel/environ.mli index f6cd41861e..2abcea148a 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -215,12 +215,6 @@ val constant_value_and_type : env -> Constant.t puniverses -> polymorphic *) val constant_context : env -> Constant.t -> Univ.AUContext.t -(** Returns the body of the constant if it has any, and the polymorphic context - it lives in. For monomorphic constant, the latter is empty, and for - polymorphic constants, the term contains De Bruijn universe variables that - need to be instantiated. *) -val body_of_constant_body : env -> Opaqueproof.opaque constant_body -> (Constr.constr * Univ.AUContext.t) option - (* These functions should be called under the invariant that [env] already contains the constraints corresponding to the constant application. *) diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 18c1bcc0f8..75f96da3eb 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -16,6 +16,11 @@ open Mod_subst type work_list = (Instance.t * Id.t array) Cmap.t * (Instance.t * Id.t array) Mindmap.t +type indirect_accessor = { + access_proof : DirPath.t -> int -> constr option; + access_constraints : DirPath.t -> int -> Univ.ContextSet.t option; +} + type cooking_info = { modlist : work_list; abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } @@ -36,20 +41,8 @@ let empty_opaquetab = { opaque_dir = DirPath.initial; } -(* hooks *) -let default_get_opaque dp _ = - CErrors.user_err Pp.(pr_sequence str ["Cannot access opaque proofs in library"; DirPath.to_string dp]) -let default_get_univ dp _ = - CErrors.user_err (Pp.pr_sequence Pp.str [ - "Cannot access universe constraints of opaque proofs in library "; - DirPath.to_string dp]) - -let get_opaque = ref default_get_opaque -let get_univ = ref default_get_univ - -let set_indirect_opaque_accessor f = (get_opaque := f) -let set_indirect_univ_accessor f = (get_univ := f) -(* /hooks *) +let not_here () = + CErrors.user_err Pp.(str "Cannot access opaque delayed proof") let create cu = Direct ([],cu) @@ -95,51 +88,52 @@ let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function let fp = snd (Int.Map.find i prfs) in join except fp -let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function +let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> fst(Future.force cu) | Indirect (l,dp,i) -> let pt = if DirPath.equal dp odp then Future.chain (snd (Int.Map.find i prfs)) fst - else !get_opaque dp i in + else match access.access_proof dp i with + | None -> not_here () + | Some v -> Future.from_val v + in let c = Future.force pt in force_constr (List.fold_right subst_substituted l (from_val c)) -let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function +let force_constraints access { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> snd(Future.force cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp then snd (Future.force (snd (Int.Map.find i prfs))) - else match !get_univ dp i with + else match access.access_constraints dp i with | None -> Univ.ContextSet.empty - | Some u -> Future.force u + | Some u -> u -let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,cu) -> Some(Future.chain cu snd) - | Indirect (_,dp,i) -> - if DirPath.equal dp odp - then Some(Future.chain (snd (Int.Map.find i prfs)) snd) - else !get_univ dp i +let get_direct_constraints = function +| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") +| Direct (_, cu) -> Future.chain cu snd module FMap = Future.UUIDMap -let a_constr = Future.from_val (mkRel 1) -let a_univ = Future.from_val Univ.ContextSet.empty -let a_discharge : cooking_info list = [] - -let dump { opaque_val = otab; opaque_len = n; _ } = - let opaque_table = Array.make n a_constr in - let univ_table = Array.make n a_univ in - let disch_table = Array.make n a_discharge in +let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } = + let opaque_table = Array.make n None in + let univ_table = Array.make n None in + let disch_table = Array.make n [] in let f2t_map = ref FMap.empty in - Int.Map.iter (fun n (d,cu) -> - let c, u = Future.split2 cu in - Future.sink u; - Future.sink c; - opaque_table.(n) <- c; - univ_table.(n) <- u; - disch_table.(n) <- d; - f2t_map := FMap.add (Future.uuid cu) n !f2t_map) - otab; + let iter n (d, cu) = + let uid = Future.uuid cu in + let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in + if Future.is_val cu then + let (c, u) = Future.force cu in + let () = univ_table.(n) <- Some u in + opaque_table.(n) <- Some c + else if Future.UUIDSet.mem uid except then + disch_table.(n) <- d + else + CErrors.anomaly + Pp.(str"Proof object "++int n++str" is not checked nor to be checked") + in + let () = Int.Map.iter iter otab in opaque_table, univ_table, disch_table, !f2t_map diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 4e8956af06..4646206e55 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -35,12 +35,20 @@ val create : proofterm -> opaque used so far *) val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab +type indirect_accessor = { + access_proof : DirPath.t -> int -> constr option; + access_constraints : DirPath.t -> int -> Univ.ContextSet.t option; +} +(** When stored indirectly, opaque terms are indexed by their library + dirpath and an integer index. The two functions above activate + this indirect storage, by telling how to retrieve terms. +*) + (** From a [opaque] back to a [constr]. This might use the - indirect opaque accessor configured below. *) -val force_proof : opaquetab -> opaque -> constr -val force_constraints : opaquetab -> opaque -> Univ.ContextSet.t -val get_constraints : - opaquetab -> opaque -> Univ.ContextSet.t Future.computation option + indirect opaque accessor given as an argument. *) +val force_proof : indirect_accessor -> opaquetab -> opaque -> constr +val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t +val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation val subst_opaque : substitution -> opaque -> opaque @@ -60,21 +68,8 @@ val discharge_direct_opaque : val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit -val dump : opaquetab -> - Constr.t Future.computation array * - Univ.ContextSet.t Future.computation array * +val dump : ?except:Future.UUIDSet.t -> opaquetab -> + Constr.t option array * + Univ.ContextSet.t option array * cooking_info list array * int Future.UUIDMap.t - -(** When stored indirectly, opaque terms are indexed by their library - dirpath and an integer index. The following two functions activate - this indirect storage, by telling how to store and retrieve terms. - Default creator always returns [None], preventing the creation of - any indirect link, and default accessor always raises an error. -*) - -val set_indirect_opaque_accessor : - (DirPath.t -> int -> constr Future.computation) -> unit -val set_indirect_univ_accessor : - (DirPath.t -> int -> Univ.ContextSet.t Future.computation option) -> unit - diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index a5d8a480ee..873cc2a172 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -458,19 +458,11 @@ let labels_of_mib mib = Array.iter visit_mip mib.mind_packets; get () -let globalize_constant_universes env cb = +let globalize_constant_universes cb = match cb.const_universes with | Monomorphic cstrs -> - Now (false, cstrs) :: - (match cb.const_body with - | (Undef _ | Def _ | Primitive _) -> [] - | OpaqueDef lc -> - match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with - | None -> [] - | Some fc -> - match Future.peek_val fc with - | None -> [Later fc] - | Some c -> [Now (false, c)]) + (* Constraints hidden in the opaque body are added by [add_constant_aux] *) + [Now (false, cstrs)] | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)] @@ -480,9 +472,9 @@ let globalize_mind_universes mb = [Now (false, ctx)] | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)] -let constraints_of_sfb env sfb = +let constraints_of_sfb sfb = match sfb with - | SFBconst cb -> globalize_constant_universes env cb + | SFBconst cb -> globalize_constant_universes cb | SFBmind mib -> globalize_mind_universes mib | SFBmodtype mtb -> [Now (false, mtb.mod_constraints)] | SFBmodule mb -> [Now (false, mb.mod_constraints)] @@ -520,7 +512,8 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv = separately. *) senv else - let cst = constraints_of_sfb senv.env sfb in + (* Delayed constraints from opaque body are added by [add_constant_aux] *) + let cst = constraints_of_sfb sfb in add_constraints_list cst senv in let env' = match sfb, gn with @@ -553,6 +546,15 @@ type exported_private_constant = let add_constant_aux ~in_section senv (kn, cb) = let l = Constant.label kn in + let delayed_cst = match cb.const_body with + | OpaqueDef o when not (Declareops.constant_is_polymorphic cb) -> + let fc = Opaqueproof.get_direct_constraints o in + begin match Future.peek_val fc with + | None -> [Later fc] + | Some c -> [Now (false, c)] + end + | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> [] + in let cb, otab = match cb.const_body with | OpaqueDef lc when not in_section -> (* In coqc, opaque constants outside sections will be stored @@ -565,6 +567,7 @@ let add_constant_aux ~in_section senv (kn, cb) = in let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in let senv' = add_field (l,SFBconst cb) (C kn) senv in + let senv' = add_constraints_list delayed_cst senv' in let senv'' = match cb.const_body with | Undef (Some lev) -> update_resolver diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 5e3a3c3347..88fcb71e77 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -11,10 +11,10 @@ open Names open Univ open Constr -(*******************************************) +(********************************************) (* Initialization of the abstract machine ***) -(* Necessary for [relaccu_tbl] *) -(*******************************************) +(* Necessary for [relaccu_tbl] *) +(********************************************) external init_vm : unit -> unit = "init_coq_vm" diff --git a/lib/pp.mli b/lib/pp.mli index 8b3a07d4b2..bc20a66824 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -18,7 +18,7 @@ (* to interpret. *) (* *) (* The datatype has a public view to allow serialization or advanced *) -(* uses, however regular users are _strongly_ warned against its use, *) +(* uses, however regular users are _strongly_ warned against its use, *) (* they should instead rely on the available functions below. *) (* *) (* Box order and number is indeed an important factor. Try to create *) diff --git a/lib/util.ml b/lib/util.ml index 38d73d3453..6e8b8de5dc 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -14,7 +14,7 @@ let on_fst f (a,b) = (f a,b) let on_snd f (a,b) = (a,f b) let map_pair f (a,b) = (f a,f b) -(* Mapping under pairs *) +(* Mapping under triplets *) let on_pi1 f (a,b,c) = (f a,b,c) let on_pi2 f (a,b,c) = (a,f b,c) diff --git a/lib/util.mli b/lib/util.mli index 1eb60f509a..9a00ee3440 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -17,7 +17,7 @@ val on_fst : ('a -> 'b) -> 'a * 'c -> 'b * 'c val on_snd : ('a -> 'b) -> 'c * 'a -> 'c * 'b val map_pair : ('a -> 'b) -> 'a * 'a -> 'b * 'b -(** Mapping under triple *) +(** Mapping under triplets *) val on_pi1 : ('a -> 'b) -> 'a * 'c * 'd -> 'b * 'c * 'd val on_pi2 : ('a -> 'b) -> 'c * 'a * 'd -> 'c * 'b * 'd diff --git a/library/global.ml b/library/global.ml index 58e2380440..d5ffae7716 100644 --- a/library/global.ml +++ b/library/global.ml @@ -132,9 +132,20 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) let opaque_tables () = Environ.opaque_tables (env ()) -let body_of_constant_body ce = body_of_constant_body (env ()) ce - -let body_of_constant cst = body_of_constant_body (lookup_constant cst) +let body_of_constant_body access env cb = + let open Declarations in + let otab = Environ.opaque_tables env in + match cb.const_body with + | Undef _ | Primitive _ -> + None + | Def c -> + Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb) + | OpaqueDef o -> + Some (Opaqueproof.force_proof access otab o, Declareops.constant_polymorphic_context cb) + +let body_of_constant_body access ce = body_of_constant_body access (env ()) ce + +let body_of_constant access cst = body_of_constant_body access (lookup_constant cst) (** Operations on kernel names *) diff --git a/library/global.mli b/library/global.mli index 984d8c666c..aa9fc18477 100644 --- a/library/global.mli +++ b/library/global.mli @@ -100,13 +100,13 @@ val mind_of_delta_kn : KerName.t -> MutInd.t val opaque_tables : unit -> Opaqueproof.opaquetab -val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option +val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t -> (Constr.constr * Univ.AUContext.t) option (** Returns the body of the constant if it has any, and the polymorphic context it lives in. For monomorphic constant, the latter is empty, and for polymorphic constants, the term contains De Bruijn universe variables that need to be instantiated. *) -val body_of_constant_body : Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option +val body_of_constant_body : Opaqueproof.indirect_accessor -> Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option (** Same as {!body_of_constant} but on {!Declarations.constant_body}. *) (** {6 Compiled libraries } *) diff --git a/library/library.ml b/library/library.ml index d8eaf5f659..039124635e 100644 --- a/library/library.ml +++ b/library/library.ml @@ -264,85 +264,6 @@ let in_import_library : DirPath.t list * bool -> obj = subst_function = subst_import_library; classify_function = classify_import_library } - -(************************************************************************) -(*s Locate absolute or partially qualified library names in the path *) - -exception LibUnmappedDir -exception LibNotFound -type library_location = LibLoaded | LibInPath - -let warn_several_object_files = - CWarnings.create ~name:"several-object-files" ~category:"require" - (fun (vi, vo) -> str"Loading" ++ spc () ++ str vi ++ - strbrk " instead of " ++ str vo ++ - strbrk " because it is more recent") - -let locate_absolute_library dir = - (* Search in loadpath *) - let pref, base = split_dirpath dir in - let loadpath = Loadpath.filter_path (fun dir -> DirPath.equal dir pref) in - let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in - let loadpath = List.map fst loadpath in - let find ext = - try - let name = Id.to_string base ^ ext in - let _, file = System.where_in_path ~warn:false loadpath name in - Some file - with Not_found -> None in - match find ".vo", find ".vio" with - | None, None -> raise LibNotFound - | Some file, None | None, Some file -> file - | Some vo, Some vi when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - vi - | Some vo, Some _ -> vo - -let locate_qualified_library ?root ?(warn = true) qid = - (* Search library in loadpath *) - let dir, base = repr_qualid qid in - let loadpath = Loadpath.expand_path ?root dir in - let () = match loadpath with [] -> raise LibUnmappedDir | _ -> () in - let find ext = - try - let name = Id.to_string base ^ ext in - let lpath, file = - System.where_in_path ~warn (List.map fst loadpath) name in - Some (lpath, file) - with Not_found -> None in - let lpath, file = - match find ".vo", find ".vio" with - | None, None -> raise LibNotFound - | Some res, None | None, Some res -> res - | Some (_, vo), Some (_, vi as resvi) - when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> - warn_several_object_files (vi, vo); - resvi - | Some resvo, Some _ -> resvo - in - let dir = add_dirpath_suffix (String.List.assoc lpath loadpath) base in - (* Look if loaded *) - if library_is_loaded dir then (LibLoaded, dir,library_full_filename dir) - (* Otherwise, look for it in the file system *) - else (LibInPath, dir, file) - -let error_unmapped_dir qid = - let prefix, _ = repr_qualid qid in - user_err ~hdr:"load_absolute_library_from" - (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ - str "no physical path bound to" ++ spc () ++ DirPath.print prefix ++ fnl ()) - -let error_lib_not_found qid = - user_err ~hdr:"load_absolute_library_from" - (str"Cannot find library " ++ pr_qualid qid ++ str" in loadpath") - -let try_locate_absolute_library dir = - try - locate_absolute_library dir - with - | LibUnmappedDir -> error_unmapped_dir (qualid_of_dirpath dir) - | LibNotFound -> error_lib_not_found (qualid_of_dirpath dir) - (************************************************************************) (** {6 Tables of opaque proof terms} *) @@ -355,8 +276,8 @@ let try_locate_absolute_library dir = (** Delayed / available tables of opaque terms *) type 'a table_status = - | ToFetch of 'a Future.computation array delayed - | Fetched of 'a Future.computation array + | ToFetch of 'a option array delayed + | Fetched of 'a option array let opaque_tables = ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t) @@ -394,12 +315,13 @@ let access_opaque_table dp i = let access_univ_table dp i = try let what = "universe contexts of opaque proofs" in - Some (access_table what univ_tables dp i) + access_table what univ_tables dp i with Not_found -> None -let () = - Opaqueproof.set_indirect_opaque_accessor access_opaque_table; - Opaqueproof.set_indirect_univ_accessor access_univ_table +let indirect_accessor = { + Opaqueproof.access_proof = access_opaque_table; + Opaqueproof.access_constraints = access_univ_table; +} (************************************************************************) (* Internalise libraries *) @@ -407,9 +329,9 @@ let () = type seg_sum = summary_disk type seg_lib = library_disk type seg_univ = (* true = vivo, false = vi *) - Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool + Univ.ContextSet.t option array * Univ.ContextSet.t * bool type seg_discharge = Opaqueproof.cooking_info list array -type seg_proofs = Constr.constr Future.computation array +type seg_proofs = Constr.constr option array let mk_library sd md digests univs = { @@ -450,7 +372,7 @@ let intern_from_file f = module DPMap = Map.Make(DirPath) -let rec intern_library (needed, contents) (dir, f) from = +let rec intern_library ~lib_resolver (needed, contents) (dir, f) from = (* Look if in the current logical environment *) try (find_library dir).libsum_digests, (needed, contents) with Not_found -> @@ -459,7 +381,7 @@ let rec intern_library (needed, contents) (dir, f) from = with Not_found -> Feedback.feedback(Feedback.FileDependency (from, DirPath.to_string dir)); (* [dir] is an absolute name which matches [f] which must be in loadpath *) - let f = match f with Some f -> f | None -> try_locate_absolute_library dir in + let f = match f with Some f -> f | None -> lib_resolver dir in let m = intern_from_file f in if not (DirPath.equal dir m.library_name) then user_err ~hdr:"load_physical_library" @@ -467,22 +389,24 @@ let rec intern_library (needed, contents) (dir, f) from = DirPath.print m.library_name ++ spc () ++ str "and not library" ++ spc() ++ DirPath.print dir); Feedback.feedback (Feedback.FileLoaded(DirPath.to_string dir, f)); - m.library_digests, intern_library_deps (needed, contents) dir m f + m.library_digests, intern_library_deps ~lib_resolver (needed, contents) dir m f -and intern_library_deps libs dir m from = - let needed, contents = Array.fold_left (intern_mandatory_library dir from) libs m.library_deps in +and intern_library_deps ~lib_resolver libs dir m from = + let needed, contents = + Array.fold_left (intern_mandatory_library ~lib_resolver dir from) + libs m.library_deps in (dir :: needed, DPMap.add dir m contents ) -and intern_mandatory_library caller from libs (dir,d) = - let digest, libs = intern_library libs (dir, None) (Some from) in +and intern_mandatory_library ~lib_resolver caller from libs (dir,d) = + let digest, libs = intern_library ~lib_resolver libs (dir, None) (Some from) in if not (Safe_typing.digest_match ~actual:digest ~required:d) then user_err (str "Compiled library " ++ DirPath.print caller ++ str " (in file " ++ str from ++ str ") makes inconsistent assumptions \ over library " ++ DirPath.print dir); libs -let rec_intern_library libs (dir, f) = - let _, libs = intern_library libs (dir, Some f) None in +let rec_intern_library ~lib_resolver libs (dir, f) = + let _, libs = intern_library ~lib_resolver libs (dir, Some f) None in libs let native_name_from_filename f = @@ -557,8 +481,8 @@ let warn_require_in_module = strbrk "You can Require a module at toplevel " ++ strbrk "and optionally Import it inside another one.") -let require_library_from_dirpath modrefl export = - let needed, contents = List.fold_left rec_intern_library ([], DPMap.empty) modrefl in +let require_library_from_dirpath ~lib_resolver modrefl export = + let needed, contents = List.fold_left (rec_intern_library ~lib_resolver) ([], DPMap.empty) modrefl in let needed = List.rev_map (fun dir -> DPMap.find dir contents) needed in let modrefl = List.map fst modrefl in if Lib.is_module_or_modtype () then @@ -667,7 +591,7 @@ let save_library_to ?todo ~output_native_objects dir f otab = List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty l in let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in - let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in + let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in let tasks, utab, dtab = match todo with | None -> None, None, None @@ -680,16 +604,6 @@ let save_library_to ?todo ~output_native_objects dir f otab = Some (tasks,rcbackup), Some (univ_table,Univ.ContextSet.empty,false), Some disch_table in - let except = - Future.UUIDSet.fold (fun uuid acc -> - try Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc - with Not_found -> acc) - except Int.Set.empty in - let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in - Array.iteri (fun i x -> - if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library" - Pp.(str"Proof object "++int i++str" is not checked nor to be checked")) - opaque_table; let sd = { md_name = dir; md_deps = Array.of_list (current_deps ()); diff --git a/library/library.mli b/library/library.mli index 390299bf56..2c0673c3b1 100644 --- a/library/library.mli +++ b/library/library.mli @@ -22,7 +22,11 @@ open Libnames (** {6 ... } Require = load in the environment + open (if the optional boolean is not [None]); mark also for export if the boolean is [Some true] *) -val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> unit +val require_library_from_dirpath + : lib_resolver:(DirPath.t -> CUnix.physical_path) + -> (DirPath.t * string) list + -> bool option + -> unit (** {6 Start the compilation of a library } *) @@ -30,9 +34,9 @@ val require_library_from_dirpath : (DirPath.t * string) list -> bool option -> u type seg_sum type seg_lib type seg_univ = (* cst, all_cst, finished? *) - Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool + Univ.ContextSet.t option array * Univ.ContextSet.t * bool type seg_discharge = Opaqueproof.cooking_info list array -type seg_proofs = Constr.constr Future.computation array +type seg_proofs = Constr.constr option array (** Open a module (or a library); if the boolean is true then it's also an export otherwise just a simple import *) @@ -45,8 +49,10 @@ val save_library_to : output_native_objects:bool -> DirPath.t -> string -> Opaqueproof.opaquetab -> unit -val load_library_todo : - string -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs +val load_library_todo + : CUnix.physical_path + -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs + val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit (** {6 Interrogate the status of libraries } *) @@ -65,20 +71,8 @@ val library_full_filename : DirPath.t -> string (** - Overwrite the filename of all libraries (used when restoring a state) *) val overwrite_library_filenames : string -> unit -(** {6 Locate a library in the load paths } *) -exception LibUnmappedDir -exception LibNotFound -type library_location = LibLoaded | LibInPath - -val locate_qualified_library : - ?root:DirPath.t -> ?warn:bool -> qualid -> - library_location * DirPath.t * CUnix.physical_path -(** Locates a library by implicit name. - - @raise LibUnmappedDir if the library is not in the path - @raise LibNotFound if there is no corresponding file in the path - -*) - (** {6 Native compiler. } *) val native_name_from_filename : string -> string + +(** {6 Opaque accessors} *) +val indirect_accessor : Opaqueproof.indirect_accessor diff --git a/library/library.mllib b/library/library.mllib index 8f694f4a31..ef53471377 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -7,7 +7,6 @@ Global Decl_kinds Lib Declaremods -Loadpath Library States Kindops diff --git a/library/loadpath.ml b/library/loadpath.ml deleted file mode 100644 index fc13c864d0..0000000000 --- a/library/loadpath.ml +++ /dev/null @@ -1,119 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -open Pp -open Util -open CErrors -open Names -open Libnames - -(** Load paths. Mapping from physical to logical paths. *) - -type t = { - path_physical : CUnix.physical_path; - path_logical : DirPath.t; - path_implicit : bool; -} - -let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" - -let logical p = p.path_logical - -let physical p = p.path_physical - -let get_load_paths () = !load_paths - -let anomaly_too_many_paths path = - anomaly (str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".") - -let find_load_path phys_dir = - let phys_dir = CUnix.canonical_path_name phys_dir in - let filter p = String.equal p.path_physical phys_dir in - let paths = List.filter filter !load_paths in - match paths with - | [] -> raise Not_found - | [p] -> p - | _ -> anomaly_too_many_paths phys_dir - -let is_in_load_paths phys_dir = - let dir = CUnix.canonical_path_name phys_dir in - let lp = get_load_paths () in - let check_p p = String.equal dir p.path_physical in - List.exists check_p lp - -let remove_load_path dir = - let filter p = not (String.equal p.path_physical dir) in - load_paths := List.filter filter !load_paths - -let warn_overriding_logical_loadpath = - CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" - (fun (phys_path, old_path, coq_path) -> - str phys_path ++ strbrk " was previously bound to " ++ - DirPath.print old_path ++ strbrk "; it is remapped to " ++ - DirPath.print coq_path) - -let add_load_path phys_path coq_path ~implicit = - let phys_path = CUnix.canonical_path_name phys_path in - let filter p = String.equal p.path_physical phys_path in - let binding = { - path_logical = coq_path; - path_physical = phys_path; - path_implicit = implicit; - } in - match List.filter filter !load_paths with - | [] -> - load_paths := binding :: !load_paths - | [{ path_logical = old_path; path_implicit = old_implicit }] -> - let replace = - if DirPath.equal coq_path old_path then - implicit <> old_implicit - else - let () = - (* Do not warn when overriding the default "-I ." path *) - if not (DirPath.equal old_path Libnames.default_root_prefix) then - warn_overriding_logical_loadpath (phys_path, old_path, coq_path) - in - true in - if replace then - begin - remove_load_path phys_path; - load_paths := binding :: !load_paths; - end - | _ -> anomaly_too_many_paths phys_path - -let filter_path f = - let rec aux = function - | [] -> [] - | p :: l -> - if f p.path_logical then (p.path_physical, p.path_logical) :: aux l - else aux l - in - aux !load_paths - -let expand_path ?root dir = - let rec aux = function - | [] -> [] - | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> - let success = - match root with - | None -> - if implicit then is_dirpath_suffix_of dir lg - else DirPath.equal dir lg - | Some root -> - is_dirpath_prefix_of root lg && - is_dirpath_suffix_of dir (drop_dirpath_prefix root lg) in - if success then (ph, lg) :: aux l else aux l in - aux !load_paths - -let locate_file fname = - let paths = List.map physical !load_paths in - let _,longfname = - System.find_file_in_path ~warn:(not !Flags.quiet) paths fname in - longfname diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 6df97609f5..bd88570224 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -31,8 +31,10 @@ let ldots_var = Id.of_string ".." let constr_kw = [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; "end"; "as"; "let"; "if"; "then"; "else"; "return"; - "SProp"; "Prop"; "Set"; "Type"; ".("; "_"; ".."; - "`{"; "`("; "{|"; "|}" ] + "SProp"; "Prop"; "Set"; "Type"; + ":="; "=>"; "->"; ".."; "<:"; "<<:"; ":>"; + ".("; "()"; "`{"; "`("; "@{"; "{|"; + "_"; "@"; "+"; "!"; "?"; ";"; ","; ":" ] let _ = List.iter CLexer.add_keyword constr_kw @@ -225,11 +227,13 @@ GRAMMAR EXTEND Gram [ c=atomic_constr -> { c } | c=match_constr -> { c } | "("; c = operconstr LEVEL "200"; ")" -> - { (match c.CAst.v with + { (* Preserve parentheses around numerals so that constrintern does not + collapse -(3) into the numeral -3. *) + (match c.CAst.v with | CPrim (Numeral (SPlus,n)) -> CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"( _ )"),([c],[],[],[])) | _ -> c) } - | "{|"; c = record_declaration; "|}" -> { c } + | "{|"; c = record_declaration; bar_cbrace -> { c } | "{"; c = binder_constr ; "}" -> { CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) } | "`{"; c = operconstr LEVEL "200"; "}" -> @@ -277,16 +281,16 @@ GRAMMAR EXTEND Gram ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CLetTuple (lb,po,c1,c2) } - | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; + | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCases (LetPatternStyle, None, [c1, None, None], [CAst.make ~loc ([[p]], c2)]) } - | "let"; "'"; p=pattern; ":="; c1 = operconstr LEVEL "200"; + | "let"; "'"; p = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ CCases (LetPatternStyle, Some rt, [c1, aliasvar p, None], [CAst.make ~loc ([[p]], c2)]) } - | "let"; "'"; p=pattern; "in"; t = pattern LEVEL "200"; + | "let"; "'"; p = pattern LEVEL "200"; "in"; t = pattern LEVEL "200"; ":="; c1 = operconstr LEVEL "200"; rt = case_type; "in"; c2 = operconstr LEVEL "200" -> { CAst.make ~loc @@ @@ -359,7 +363,7 @@ GRAMMAR EXTEND Gram case_item: [ [ c=operconstr LEVEL "100"; ona = OPT ["as"; id=name -> { id } ]; - ty = OPT ["in"; t=pattern -> { t } ] -> + ty = OPT ["in"; t = pattern LEVEL "200" -> { t } ] -> { (c,ona,ty) } ] ] ; case_type: @@ -377,14 +381,14 @@ GRAMMAR EXTEND Gram [ [ OPT"|"; br=LIST0 eqn SEP "|" -> { br } ] ] ; mult_pattern: - [ [ pl = LIST1 pattern LEVEL "99" SEP "," -> { pl } ] ] + [ [ pl = LIST1 pattern LEVEL "200" SEP "," -> { pl } ] ] ; eqn: [ [ pll = LIST1 mult_pattern SEP "|"; "=>"; rhs = lconstr -> { (CAst.make ~loc (pll,rhs)) } ] ] ; record_pattern: - [ [ id = global; ":="; pat = pattern -> { (id, pat) } ] ] + [ [ id = global; ":="; pat = pattern LEVEL "200" -> { (id, pat) } ] ] ; record_patterns: [ [ p = record_pattern; ";"; ps = record_patterns -> { p :: ps } @@ -396,7 +400,10 @@ GRAMMAR EXTEND Gram pattern: [ "200" RIGHTA [ ] | "100" RIGHTA - [ p = pattern; "|"; pl = LIST1 pattern SEP "|" -> { CAst.make ~loc @@ CPatOr (p::pl) } ] + [ p = pattern; ":"; ty = binder_constr -> + {CAst.make ~loc @@ CPatCast (p, ty) } + | p = pattern; ":"; ty = operconstr LEVEL "100" -> + {CAst.make ~loc @@ CPatCast (p, ty) } ] | "99" RIGHTA [ ] | "90" RIGHTA [ ] | "10" LEFTA @@ -409,21 +416,17 @@ GRAMMAR EXTEND Gram [ c = pattern; "%"; key=IDENT -> { CAst.make ~loc @@ CPatDelimiters (key,c) } ] | "0" [ r = Prim.reference -> { CAst.make ~loc @@ CPatAtom (Some r) } - | "{|"; pat = record_patterns; "|}" -> { CAst.make ~loc @@ CPatRecord pat } + | "{|"; pat = record_patterns; bar_cbrace -> { CAst.make ~loc @@ CPatRecord pat } | "_" -> { CAst.make ~loc @@ CPatAtom None } | "("; p = pattern LEVEL "200"; ")" -> - { (match p.CAst.v with + { (* Preserve parentheses around numerals so that constrintern does not + collapse -(3) into the numeral -3. *) + (match p.CAst.v with | CPatPrim (Numeral (SPlus,n)) -> CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) | _ -> p) } - | "("; p = pattern LEVEL "200"; ":"; ty = lconstr; ")" -> - { let p = - match p with - | { CAst.v = CPatPrim (Numeral (SPlus,n)) } -> - CAst.make ~loc @@ CPatNotation((InConstrEntrySomeLevel,"( _ )"),([p],[]),[]) - | _ -> p - in - CAst.make ~loc @@ CPatCast (p, ty) } + | "("; p = pattern LEVEL "200"; "|" ; pl = LIST1 pattern LEVEL "200" SEP "|"; ")" -> + { CAst.make ~loc @@ CPatOr (p::pl) } | n = NUMERAL-> { CAst.make ~loc @@ CPatPrim (Numeral (SPlus,n)) } | s = string -> { CAst.make ~loc @@ CPatPrim (String s) } ] ] ; diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 80dd997860..9653964262 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -15,7 +15,7 @@ open Libnames open Pcoq.Prim -let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"] +let prim_kw = ["{"; "}"; "["; "]"; "("; ")"; "'"; "%"; "|"] let _ = List.iter CLexer.add_keyword prim_kw @@ -31,13 +31,19 @@ let my_int_of_string loc s = with Failure _ -> CErrors.user_err ~loc (Pp.str "This number is too large.") +let check_nospace loc expected = + let (bp, ep) = Loc.unloc loc in + if ep = bp + String.length expected then () else + Gramlib.Ploc.raise loc (Stream.Error ("'" ^ expected ^ "' expected")) + } GRAMMAR EXTEND Gram GLOBAL: bigint natural integer identref name ident var preident fullyqualid qualid reference dirpath ne_lstring - ne_string string lstring pattern_ident pattern_identref by_notation smart_global; + ne_string string lstring pattern_ident pattern_identref by_notation + smart_global bar_cbrace; preident: [ [ s = IDENT -> { s } ] ] ; @@ -123,4 +129,7 @@ GRAMMAR EXTEND Gram bigint: (* Negative numbers are dealt with elsewhere *) [ [ i = NUMERAL -> { check_int loc i } ] ] ; + bar_cbrace: + [ [ "|"; "}" -> { check_nospace loc "|}" } ] ] + ; END diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index a78ad4f842..b474c8e9a9 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -411,6 +411,8 @@ module Prim = let ne_string = Entry.create "Prim.ne_string" let ne_lstring = Entry.create "Prim.ne_lstring" + let bar_cbrace = Entry.create "'|}'" + end module Constr = diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 3a57c14a3b..5f982346ab 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -38,9 +38,9 @@ end - dynamic rules declared at the evaluation of Coq files (using e.g. Notation, Infix, or Tactic Notation) - - static rules explicitly defined in files g_*.ml4 + - static rules explicitly defined in files g_*.mlg - static rules macro-generated by ARGUMENT EXTEND, TACTIC EXTEND and - VERNAC EXTEND (see e.g. file extratactics.ml4) + VERNAC EXTEND (see e.g. file extratactics.mlg) Note that parsing a Coq document is in essence stateful: the parser needs to recognize commands that start proofs and use a different @@ -170,6 +170,7 @@ module Prim : val ne_string : string Entry.t val ne_lstring : lstring Entry.t val var : lident Entry.t + val bar_cbrace : unit Entry.t end module Constr : diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 9db7c8d8d3..051d1f8e0f 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -115,7 +115,7 @@ let get_body lconstr = EConstr.of_constr (Mod_subst.force_constr lconstr) let get_opaque env c = EConstr.of_constr - (Opaqueproof.force_proof (Environ.opaque_tables env) c) + (Opaqueproof.force_proof Library.indirect_accessor (Environ.opaque_tables env) c) let applistc c args = EConstr.mkApp (c, Array.of_list args) diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index cffe8a3e78..f2b9ba2ec6 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -951,7 +951,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num (* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *) let f_def = Global.lookup_constant (fst (destConst evd f)) in let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in - let (f_body, _) = Option.get (Global.body_of_constant_body f_def) in + let (f_body, _) = Option.get (Global.body_of_constant_body Library.indirect_accessor f_def) in let f_body = EConstr.of_constr f_body in let params,f_body_with_params = decompose_lam_n evd nb_params f_body in let (_,num),(_,_,bodies) = destFix evd f_body_with_params in @@ -1082,7 +1082,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam } in let get_body const = - match Global.body_of_constant const with + match Global.body_of_constant Library.indirect_accessor const with | Some (body, _) -> let env = Global.env () in let sigma = Evd.from_env env in diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index f51c6dc6be..2c107d39d9 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -413,7 +413,7 @@ let get_funs_constant mp = in function const -> let find_constant_body const = - match Global.body_of_constant const with + match Global.body_of_constant Library.indirect_accessor const with | Some (body, _) -> let body = Tacred.cbv_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index ce7d149ae1..a6b088de0c 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -851,7 +851,7 @@ let make_graph ~pstate (f_ref : GlobRef.t) = end | _ -> raise (UserError (None, str "Not a function reference") ) in - (match Global.body_of_constant_body c_body with + (match Global.body_of_constant_body Library.indirect_accessor c_body with | None -> error "Cannot build a graph over an axiom!" | Some (body, _) -> let env = Global.env () in diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index f5098d2a34..4c186dce09 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -146,6 +146,23 @@ let discrHyp id = let injection_main with_evars c = elimOnConstrWithHoles (injClause None None) with_evars c +let isInjPat pat = match pat.CAst.v with IntroAction (IntroInjection _) -> Some pat.CAst.loc | _ -> None + +let decode_inj_ipat ?loc = function + (* For the "as [= pat1 ... patn ]" syntax *) + | [{ CAst.v = IntroAction (IntroInjection ipat) }] -> ipat + (* For the "as pat1 ... patn" syntax *) + | ([] | [_]) as ipat -> ipat + | pat1::pat2::_ as ipat -> + (* To be sure that there is no confusion of syntax, we check that no [= ...] occurs + in the non-singleton list of patterns *) + match isInjPat pat1 with + | Some _ -> user_err ?loc:pat2.CAst.loc (str "Unexpected pattern.") + | None -> + match List.map_filter isInjPat ipat with + | loc :: _ -> user_err ?loc (str "Unexpected injection pattern.") + | [] -> ipat + } TACTIC EXTEND injection @@ -158,15 +175,15 @@ TACTIC EXTEND einjection END TACTIC EXTEND injection_as | [ "injection" "as" intropattern_list(ipat)] -> - { injClause None (Some ipat) false None } + { injClause None (Some (decode_inj_ipat ipat)) false None } | [ "injection" destruction_arg(c) "as" intropattern_list(ipat)] -> - { mytclWithHoles (injClause None (Some ipat)) false c } + { mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) false c } END TACTIC EXTEND einjection_as | [ "einjection" "as" intropattern_list(ipat)] -> - { injClause None (Some ipat) true None } + { injClause None (Some (decode_inj_ipat ipat)) true None } | [ "einjection" destruction_arg(c) "as" intropattern_list(ipat)] -> - { mytclWithHoles (injClause None (Some ipat)) true c } + { mytclWithHoles (injClause None (Some (decode_inj_ipat ipat))) true c } END TACTIC EXTEND simple_injection | [ "simple" "injection" ] -> { simpleInjClause None false None } diff --git a/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v index 36ed0210e3..b20f45af3e 100644 --- a/plugins/micromega/EnvRing.v +++ b/plugins/micromega/EnvRing.v @@ -925,7 +925,7 @@ Qed. revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. - discriminate. - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. - * injection H as <-. rewrite <- PSubstL1_ok; intuition. + * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition. * now apply IH. Qed. diff --git a/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v index 4886c8b9aa..9be2535a3f 100644 --- a/plugins/setoid_ring/InitialRing.v +++ b/plugins/setoid_ring/InitialRing.v @@ -105,7 +105,7 @@ Section ZMORPHISM. Proof. constructor. destruct c;intros;try discriminate. - injection H as <-. + injection H as [= <-]. simpl. unfold Zeq_bool. rewrite Z.compare_refl. trivial. Qed. diff --git a/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v index f7cb6b688b..c5d396427b 100644 --- a/plugins/setoid_ring/Ring_polynom.v +++ b/plugins/setoid_ring/Ring_polynom.v @@ -894,7 +894,7 @@ Section MakeRingPol. revert P1. induction LM1 as [|(M2,P2') LM2 IH]; simpl; intros. - discriminate. - assert (H':=PNSubst_ok n P3 M2 P2'). destruct PNSubst. - * injection H as <-. rewrite <- PSubstL1_ok; intuition. + * injection H as [= <-]. rewrite <- PSubstL1_ok; intuition. * now apply IH. Qed. diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 59fc69f100..538d0c4e9a 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -313,7 +313,7 @@ let rw_progress rhs lhs ise = not (EConstr.eq_constr ise lhs (Evarutil.nf_evar i (* Coq has a more general form of "equation" (any type with a single *) (* constructor with no arguments with_rect_r elimination lemmas). *) (* However there is no clear way of determining the LHS and RHS of *) -(* such a generic Leibniz equation -- short of inspecting the type *) +(* such a generic Leibniz equation -- short of inspecting the type *) (* of the elimination lemmas. *) let rec strip_prod_assum c = match Constr.kind c with diff --git a/pretyping/cases.ml b/pretyping/cases.ml index d7a6c4c832..fadf290d44 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -824,7 +824,7 @@ let push_alias_eqn sigma alias eqn = (**********************************************************************) (* Functions to deal with elimination predicate *) -(* Infering the predicate *) +(* Inferring the predicate *) (* The problem to solve is the following: @@ -1455,7 +1455,7 @@ let compile ~program_mode sigma pb = (* Building the sub-problem when all patterns are variables. Case - where [current] is an intially pushed term. *) + where [current] is an initially pushed term. *) and shift_problem ((current,t),_,na) sigma pb = let ty = type_of_tomatch t in let tomatch = lift_tomatch_stack 1 pb.tomatch in @@ -1542,7 +1542,7 @@ let compile ~program_mode sigma pb = mat = List.map drop_alias_eqn pb.mat } in compile sigma pb in - (* If the "match" was orginally over a variable, as in "match x with + (* If the "match" was originally over a variable, as in "match x with O => true | n => n end", we give preference to non-expansion in the default clause (i.e. "match x with O => true | n => n end" rather than "match x with O => true | S p => S p end"; @@ -2067,7 +2067,7 @@ let prepare_predicate ?loc ~program_mode typing_fun env sigma tomatchs arsign ty let p2 = prepare_predicate_from_arsign_tycon ~program_mode env sigma loc tomatchs arsign t in (* Third strategy: we take the type constraint as it is; of course we could *) - (* need something inbetween, abstracting some but not all of the dependencies *) + (* need something in between, abstracting some but not all of the dependencies *) (* the "inversion" strategy deals with that but unification may not be *) (* powerful enough so strategy 2 and 3 helps; moreover, inverting does not *) (* work (yet) when a constructor has a type not precise enough for the inversion *) diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 5ea9b79336..4aa55e4d0d 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -477,7 +477,7 @@ and cbv_stack_value info env = function cbv_stack_value info env (CONSTR(c, [||]), stack_app args stk) | Some v -> cbv_stack_value info env (v,stk) | None -> mkSTACK(PRIMITIVE(op,c,args), stk) - else (* partical application *) + else (* partial application *) (assert (stk = TOP); PRIMITIVE(op,c,appl)) diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index eae961714d..04f54a1ad4 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -34,7 +34,7 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error ([unify_delay]) and another that tries to solve such remaining constraints using heuristics ([unify]). *) -(** Theses functions allow to pass arbitrary flags to the unifier and can delay constraints. +(** These functions allow to pass arbitrary flags to the unifier and can delay constraints. In case the flags are not specified, they default to [default_flags_of TransparentState.full] currently. diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 4a941a68b1..c8b1c62db0 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -284,9 +284,9 @@ let noccur_evar env evd evk c = in try occur_rec false (0,env) c; true with Occur -> false -(***************************************) -(* Managing chains of local definitons *) -(***************************************) +(****************************************) +(* Managing chains of local definitions *) +(****************************************) type alias = | RelAlias of int @@ -629,7 +629,7 @@ let solve_pattern_eqn env sigma l c = * If a variable and an alias of it are bound to the same instance, we skip * the alias (we just use eq_constr -- instead of conv --, since anyway, * only instances that are variables -- or evars -- are later considered; - * morever, we can bet that similar instances came at some time from + * moreover, we can bet that similar instances came at some time from * the very same substitution. The removal of aliased duplicates is * useful to ensure the uniqueness of a projection. *) @@ -1738,7 +1738,7 @@ let reconsider_unif_constraints unify flags evd = * Returns an optional list of evars that were instantiated, or None * if the problem couldn't be solved. *) -(* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *) +(* Rq: incomplete algorithm if pbty = CONV_X_LEQ ! *) let solve_simple_eqn unify flags ?(choose=false) ?(imitate_defs=true) env evd (pbty,(evk1,args1 as ev1),t2) = try diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index cdd36bbba6..bfe3423b11 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -40,7 +40,7 @@ type t val make : hypnaming:naming_mode -> env -> evar_map -> ltac_var_map -> t -(** Export the underlying environement *) +(** Export the underlying environment *) val env : t -> env diff --git a/pretyping/program.mli b/pretyping/program.mli index a8f5115788..2614e181d6 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -11,7 +11,7 @@ open Names open EConstr -(** A bunch of Coq constants used by Progam *) +(** A bunch of Coq constants used by Program *) val sig_typ : unit -> GlobRef.t val sig_intro : unit -> GlobRef.t diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 85e6f51387..2fc9dc2776 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -886,7 +886,7 @@ module CredNative = RedNative(CNativeEntries) (** Generic reduction function with environment Here is where unfolded constant are stored in order to be - eventualy refolded. + eventually refolded. If tactic_mode is true, it uses ReductionBehaviour, prefers refold constant instead of value and tries to infer constants @@ -1315,7 +1315,7 @@ let whd_allnolet_stack env = let whd_allnolet env = red_of_state_red (whd_allnolet_state env) -(* 4. Ad-hoc eta reduction, does not subsitute evars *) +(* 4. Ad-hoc eta reduction, does not substitute evars *) let shrink_eta c = Stack.zip Evd.empty (local_whd_state_gen eta Evd.empty (c,Stack.empty)) diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index ee27aea93f..26801d285e 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -62,7 +62,7 @@ type typeclass = { (* Context of definitions and properties on defs, will not be shared *) cl_props : Constr.rel_context; - (* The method implementaions as projections. *) + (* The method implementations as projections. *) cl_projs : (Name.t * (direction * hint_info) option * Constant.t option) list; diff --git a/pretyping/unification.ml b/pretyping/unification.ml index d134c7319f..ad69cb2890 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1219,12 +1219,12 @@ let merge_instances env sigma flags st1 st2 c1 c2 = * bindings. This may or may not close off all RHSs of * the EVARs. For each EVAR whose RHS is closed off, * we can just apply it, and go on. For each which - * is not closed off, we need to do a mimick step - + * is not closed off, we need to do a mimic step - * in general, we have something like: * * ?X == (c e1 e2 ... ei[Meta(k)] ... en) * - * so we need to do a mimick step, converting ?X + * so we need to do a mimic step, converting ?X * into * * ?X -> (c ?z1 ... ?zn) @@ -1247,7 +1247,7 @@ let merge_instances env sigma flags st1 st2 c1 c2 = * we can reverse the equation, put it into our metavar * substitution, and keep going. * - * The most efficient mimick possible is, for each + * The most efficient mimic possible is, for each * Meta-var remaining in the term, to declare a * new EVAR of the same type. This is supposedly * determinable from the clausale form context - diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 9d3ed40f6c..8d5213b988 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -249,7 +249,7 @@ let tag_var = tag Tag.variable str"@{" ++ hov 0 (prlist_with_sep pr_semicolon f (List.rev l)) ++ str"}")) let las = lapp - let lpator = 100 + let lpator = 0 let lpatrec = 0 let rec pr_patt sep inh p = @@ -283,7 +283,8 @@ let tag_var = tag Tag.variable pr_reference r, latom | CPatOr pl -> - hov 0 (prlist_with_sep pr_spcbar (pr_patt mt (lpator,L)) pl), lpator + let pp = pr_patt mt (lpator,Any) in + surround (hov 0 (prlist_with_sep pr_spcbar pp pl)), lpator | CPatNotation ((_,"( _ )"),([p],[]),[]) -> pr_patt (fun()->str"(") (max_int,E) p ++ str")", latom @@ -348,7 +349,7 @@ let tag_var = tag Tag.variable hov 1 (str "`" ++ (surround_impl b' (pr_lident CAst.(make ?loc id) ++ str " : " ++ (if t' then str "!" else mt()) ++ pr t))) - |_ -> anomaly (Pp.str "List of generalized binders have alwais one element.") + |_ -> anomaly (Pp.str "List of generalized binders have always one element.") end | Default b -> match t with diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 9541ea5882..fca33a24bf 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -549,7 +549,7 @@ let print_instance sigma cb = let print_constant with_values sep sp udecl = let cb = Global.lookup_constant sp in - let val_0 = Global.body_of_constant_body cb in + let val_0 = Global.body_of_constant_body Library.indirect_accessor cb in let typ = cb.const_type in let univs = let open Univ in @@ -557,7 +557,7 @@ let print_constant with_values sep sp udecl = match cb.const_body with | Undef _ | Def _ | Primitive _ -> cb.const_universes | OpaqueDef o -> - let body_uctxs = Opaqueproof.force_constraints otab o in + let body_uctxs = Opaqueproof.force_constraints Library.indirect_accessor otab o in match cb.const_universes with | Monomorphic ctx -> Monomorphic (ContextSet.union body_uctxs ctx) @@ -717,7 +717,7 @@ let print_full_pure_context env sigma = | OpaqueDef lc -> str "Theorem " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++ - str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof (Global.opaque_tables ()) lc) + str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc) | Def c -> str "Definition " ++ print_basename con ++ cut () ++ str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++ diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index f378a5d2dd..abb0d55b39 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -408,7 +408,7 @@ the call to db_goal_map and entering the following: let match_goals ot nt = let nevar_to_oevar = ref StringMap.empty in (* ogname is "" when there is no difference on the current path. - It's set to the old goal's evar name once a rewitten goal is found, + It's set to the old goal's evar name once a rewritten goal is found, at which point the code only searches for the replacing goals (and ot is set to nt). *) let iter2 f l1 l2 = diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index c36b0fa337..b022f4596d 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -19,7 +19,7 @@ open Reduction open Clenv (* This function put casts around metavariables whose type could not be - * infered by the refiner, that is head of applications, predicates and + * inferred by the refiner, that is head of applications, predicates and * subject of Cases. * Does check that the casted type is closed. Anyway, the refiner would * fail in this case... *) diff --git a/proofs/refine.mli b/proofs/refine.mli index 55dafe521f..b8948a92f3 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -9,7 +9,7 @@ (************************************************************************) (** The primitive refine tactic used to fill the holes in partial proofs. This - is the recommanded way to write tactics when the proof term is easy to + is the recommended way to write tactics when the proof term is easy to write down. Note that this is not the user-level refine tactic defined in Ltac which is actually based on the one below. *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index bce227dabb..799f4a380b 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -289,7 +289,7 @@ let tclIFTHENTRYELSEMUST tac1 tac2 gl = (* Fails if a tactic did not solve the goal *) let tclCOMPLETE tac = tclTHEN tac (tclFAIL_s "Proof is not complete.") -(* Try the first thats solves the current goal *) +(* Try the first that solves the current goal *) let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) diff --git a/stm/stm.ml b/stm/stm.ml index fc539b5208..e32b6c9f1c 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1837,22 +1837,18 @@ end = struct (* {{{ *) let o = match c.Declarations.const_body with | Declarations.OpaqueDef o -> o | _ -> assert false in - let uc = - Option.get - (Opaqueproof.get_constraints (Global.opaque_tables ()) o) in + (* No need to delay the computation, the future has been forced by + the call to [check_task_aux] above. *) + let uc = Opaqueproof.force_constraints Library.indirect_accessor (Global.opaque_tables ()) o in + let uc = Univ.hcons_universe_context_set uc in (* We only manipulate monomorphic terms here. *) let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in - let pr = - Future.from_val (map (Option.get (Global.body_of_constant_body c))) in - let uc = - Future.chain uc Univ.hcons_universe_context_set in - let pr = Future.chain pr discharge in - let pr = Future.chain pr Constr.hcons in - Future.sink pr; - let extra = Future.join uc in - u.(bucket) <- uc; - p.(bucket) <- pr; - u, Univ.ContextSet.union cst extra, false + let pr = map (Option.get (Global.body_of_constant_body Library.indirect_accessor c)) in + let pr = discharge pr in + let pr = Constr.hcons pr in + u.(bucket) <- Some uc; + p.(bucket) <- Some pr; + u, Univ.ContextSet.union cst uc, false let check_task name l i = match check_task_aux "" name l i with @@ -2661,16 +2657,16 @@ end (* }}} *) (********************************* STM API ************************************) (******************************************************************************) -(* Main initalization routine *) +(* Main initialization routine *) type stm_init_options = { (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should dissappear at some + specified [doc_type]. This distinction should disappear at some some point. *) doc_type : stm_doc_type; (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) - iload_path : Mltop.coq_path list; + iload_path : Loadpath.coq_path list; (* Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, @@ -2702,8 +2698,8 @@ let dirpath_of_file f = Loadpath.logical lp with Not_found -> Libnames.default_root_prefix in - let file = Filename.chop_extension (Filename.basename f) in - let id = Id.of_string file in + let f = try Filename.chop_extension (Filename.basename f) with Invalid_argument _ -> f in + let id = Id.of_string f in let ldir = Libnames.add_dirpath_suffix ldir0 id in ldir @@ -2728,7 +2724,7 @@ let new_doc { doc_type ; iload_path; require_libs; stm_options } = (* Set load path; important, this has to happen before we declare the library below as [Declaremods/Library] will infer the module name by looking at the load path! *) - List.iter Mltop.add_coq_path iload_path; + List.iter Loadpath.add_coq_path iload_path; Safe_typing.allow_delayed_constants := !cur_opt.async_proofs_mode <> APoff; @@ -3117,7 +3113,7 @@ let ind_len_loc_of_id sid = let compute_indentation ?loc sid = Option.cata (fun loc -> let open Loc in - (* The effective lenght is the lenght on the last line *) + (* The effective length is the length on the last line *) let len = loc.ep - loc.bp in let prev_indent = match ind_len_loc_of_id sid with | None -> 0 diff --git a/stm/stm.mli b/stm/stm.mli index a0bbe05b3a..5e1e9bf5ad 100644 --- a/stm/stm.mli +++ b/stm/stm.mli @@ -50,7 +50,7 @@ type stm_doc_type = | VioDoc of string (* file path *) | Interactive of interactive_top (* module path *) -(** Coq initalization options: +(** Coq initialization options: - [doc_type]: Type of document being created. @@ -63,13 +63,13 @@ type stm_doc_type = *) type stm_init_options = { (* The STM will set some internal flags differently depending on the - specified [doc_type]. This distinction should dissappear at some + specified [doc_type]. This distinction should disappear at some some point. *) doc_type : stm_doc_type; (* Initial load path in scope for the document. Usually extracted from -R options / _CoqProject *) - iload_path : Mltop.coq_path list; + iload_path : Loadpath.coq_path list; (* Require [require_libs] before the initial state is ready. Parameters follow [Library], that is to say, @@ -86,7 +86,7 @@ type stm_init_options = { (** The type of a STM document *) type doc -(** [init_core] performs some low-level initalization; should go away +(** [init_core] performs some low-level initialization; should go away in future releases. *) val init_core : unit -> unit diff --git a/tactics/abstract.ml b/tactics/abstract.ml index 6dd9a976f9..a5b2f99457 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -99,7 +99,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = (* This is important: The [Global] and [Proof Theorem] parts of the goal_kind are not relevant here as build_constant_by_tactic does use the noop terminator; but beware if some day we remove the - redundancy on constrant declaration. This opens up an interesting + redundancy on constant declaration. This opens up an interesting question, how does abstract behave when discharge is local for example? *) let goal_kind, suffix = if opaque @@ -164,7 +164,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = let inst = match const.Entries.const_entry_universes with | Entries.Monomorphic_entry _ -> EInstance.empty | Entries.Polymorphic_entry (_, ctx) -> - (* We mimick what the kernel does, that is ensuring that no additional + (* We mimic what the kernel does, that is ensuring that no additional constraints appear in the body of polymorphic constants. Ideally this should be enforced statically. *) let (_, body_uctx), _ = Future.force const.Entries.const_entry_body in diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 1fae4c3d9d..1170c1acd0 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -30,7 +30,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = if check_scheme kind ind then (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the - apropriate type *) + appropriate type *) let cte, eff = find_scheme kind ind in let sigma, cte = Evd.fresh_constant_instance env sigma cte in let c = mkConstU cte in diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index e75a61d0c6..1a0b7f84cf 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -30,7 +30,7 @@ open Proofview.Notations open Tacmach.New open Tactypes -(* This file containts the implementation of the tactics ``Decide +(* This file contains the implementation of the tactics ``Decide Equality'' and ``Compare''. They can be used to decide the propositional equality of two objects that belongs to a small inductive datatype --i.e., an inductive set such that all the diff --git a/tactics/equality.mli b/tactics/equality.mli index 6f3e08ea02..7381d5f77b 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -132,7 +132,7 @@ val subst_all : ?flags:subst_tactic_flags -> unit -> unit Proofview.tactic (* Replace term *) (* [replace_term dir_opt c cl] - perfoms replacement of [c] by the first value found in context + performs replacement of [c] by the first value found in context (according to [dir] if given to get the rewrite direction) in the clause [cl] *) val replace_term : bool option -> constr -> clause -> unit Proofview.tactic diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index e1dad9ad20..5ac28cb9e2 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -25,7 +25,7 @@ open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration (* I implemented the following functions which test whether a term t - is an inductive but non-recursive type, a general conjuction, a + is an inductive but non-recursive type, a general conjunction, a general disjunction, or a type with no constructors. They are more general than matching with or_term, and_term, etc, diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index b8c3ddb0f0..696b11d9db 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -35,7 +35,7 @@ open Coqlib contained in the arguments of the application *) (** I implemented the following functions which test whether a term [t] - is an inductive but non-recursive type, a general conjuction, a + is an inductive but non-recursive type, a general conjunction, a general disjunction, or a type with no constructors. They are more general than matching with [or_term], [and_term], etc, diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 6efa1ece9c..8cc481e30e 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -98,7 +98,7 @@ let get_local_sign sign = in List.fold_right add_local lid nil_sign *) -(* returs the identifier of lid that was the latest declared in sign. +(* returns the identifier of lid that was the latest declared in sign. * (i.e. is the identifier id of lid such that * sign_length (sign_prefix id sign) > sign_length (sign_prefix id' sign) > * for any id'<>id in lid). diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index dcd63fe760..59fd8b37d6 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -481,7 +481,7 @@ module New = struct ) <*> tclUNIT res - (* Try the first thats solves the current goal *) + (* Try the first that solves the current goal *) let tclSOLVE tacl = tclFIRST (List.map tclCOMPLETE tacl) let tclPROGRESS t = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9dafa8bad9..191f00d104 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3019,14 +3019,14 @@ let specialize (c,lbind) ipat = (* We grab names used in product to remember them at re-abstracting phase *) let typ_of_c_hd = pf_get_type_of gl c_hd in let lprod, concl = decompose_prod_assum sigma typ_of_c_hd in - (* accumulator args: arguments to apply to c_hd: all infered + (* accumulator args: arguments to apply to c_hd: all inferred args + re-abstracted rels *) let rec rebuild_lambdas sigma lprd args hd l = match lprd , l with | _, [] -> sigma,applist (hd, (List.map (nf_evar sigma) args)) | Context.Rel.Declaration.LocalAssum(nme,_)::lp' , t::l' when occur_meta sigma t -> (* nme has not been resolved, let us re-abstract it. Same - name but type updated by instanciation of other args. *) + name but type updated by instantiation of other args. *) let sigma,new_typ_of_t = Typing.type_of clause.env sigma t in let r = Retyping.relevance_of_type env sigma new_typ_of_t in let liftedargs = List.map liftrel args in @@ -4292,7 +4292,7 @@ let induction_tac with_evars params indvars elim = let elimc = contract_letin_in_lam_header sigma elimc in let elimc = mkCast (elimc, DEFAULTcast, elimt) in let elimclause = Tacmach.New.pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in - (* elimclause' is built from elimclause by instanciating all args and params. *) + (* elimclause' is built from elimclause by instantiating all args and params. *) let elimclause' = recolle_clenv i params indvars elimclause gl in (* one last resolution (useless?) *) let resolved = clenv_unique_resolver ~flags:(elim_flags ()) elimclause' gl in diff --git a/test-suite/bugs/closed/bug_2137.v b/test-suite/bugs/closed/bug_2137.v index b1f54b1766..981cc94dc1 100644 --- a/test-suite/bugs/closed/bug_2137.v +++ b/test-suite/bugs/closed/bug_2137.v @@ -3,7 +3,7 @@ The fsetdec tactic is sensitive to which way round the arguments to <> are. In the small, self-contained example below, it is able to solve the goal if it knows that "b <> a", but not if it knows that "a <> b". I would expect -it to be able to solve hte goal in either case. +it to be able to solve the goal in either case. I have coq r12238. diff --git a/test-suite/bugs/closed/bug_2603.v b/test-suite/bugs/closed/bug_2603.v index 371bfdc575..64c656a7a6 100644 --- a/test-suite/bugs/closed/bug_2603.v +++ b/test-suite/bugs/closed/bug_2603.v @@ -3,7 +3,7 @@ As noticed by A. Appel in bug #2603, module names and definition names used to be in the same namespace. But conflict with names of constructors (or 2nd mutual inductive...) used to not be checked -enough, leading to stange situations. +enough, leading to strange situations. - In 8.3pl3 we introduced checks that forbid uniformly the following situations. diff --git a/test-suite/bugs/closed/bug_3080.v b/test-suite/bugs/closed/bug_3080.v index 36ab7ff599..06719653fe 100644 --- a/test-suite/bugs/closed/bug_3080.v +++ b/test-suite/bugs/closed/bug_3080.v @@ -15,4 +15,4 @@ Notation " g ∘ f " := (compose g f) (at level 40, left associativity) : function_scope. Fail Check (fun x => x) ∘ (fun x => x). (* this [Check] should fail, as [function_scope] is not opened *) -Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arugments to [compose] *) +Check compose ((fun x => x) ∘ (fun x => x)) (fun x => x). (* this check should succeed, as [function_scope] should be automatically bound in the arguments to [compose] *) diff --git a/test-suite/bugs/closed/bug_4503.v b/test-suite/bugs/closed/bug_4503.v index 5162f352df..26731e3292 100644 --- a/test-suite/bugs/closed/bug_4503.v +++ b/test-suite/bugs/closed/bug_4503.v @@ -29,7 +29,7 @@ End ILogic. Set Printing Universes. -(* There is stil a problem if the class is universe polymorphic *) +(* There is still a problem if the class is universe polymorphic *) Section Embed_ILogic_Pre. Polymorphic Universes A T. Fail Context {A : Type@{A}} {ILA: ILogic.ILogic@{A} A}. diff --git a/test-suite/bugs/closed/bug_4720.v b/test-suite/bugs/closed/bug_4720.v index 704331e784..a870792c39 100644 --- a/test-suite/bugs/closed/bug_4720.v +++ b/test-suite/bugs/closed/bug_4720.v @@ -34,7 +34,7 @@ End WithModPriv. identical by the extraction. In Coq 8.5 and 8.6, the extractions of WithMod, WithDef, WithModPriv - were all causing Anomaly or Assert Failure. This shoud be fixed now. + were all causing Anomaly or Assert Failure. This should be fixed now. *) Require Extraction. diff --git a/test-suite/bugs/closed/bug_5123.v b/test-suite/bugs/closed/bug_5123.v index 17231bffcf..a4029aeee0 100644 --- a/test-suite/bugs/closed/bug_5123.v +++ b/test-suite/bugs/closed/bug_5123.v @@ -28,6 +28,6 @@ Goal True. opose (@vect_sigT_eqdec _ _ _ _) as H. Unshelve. all:cycle 3. - eapply existT. (*This does no typeclass resultion, which is correct.*) + eapply existT. (*This does no typeclass resolution, which is correct.*) Focus 5. Abort. diff --git a/test-suite/bugs/closed/bug_5149.v b/test-suite/bugs/closed/bug_5149.v index ae32217057..b56abfe42e 100644 --- a/test-suite/bugs/closed/bug_5149.v +++ b/test-suite/bugs/closed/bug_5149.v @@ -36,7 +36,7 @@ Proof. solve [ unshelve (subst; eapply interpf_SmartVarVar; eassumption) ] || fail "too early". Undo. - (** Implicitely at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *) + (** Implicitly at the dot. The first fails because unshelve adds a goal, and solve hence fails. The second has an ambiant unification problem that is solved after solve *) Fail solve [ unshelve (eapply interpf_SmartVarVar; subst; eassumption) ]. solve [eapply interpf_SmartVarVar; subst; eassumption]. Undo. diff --git a/test-suite/bugs/closed/bug_808_2411.v b/test-suite/bugs/closed/bug_808_2411.v index 1169b2036b..9fe4c9d503 100644 --- a/test-suite/bugs/closed/bug_808_2411.v +++ b/test-suite/bugs/closed/bug_808_2411.v @@ -2,7 +2,7 @@ Section test. Variable n:nat. Lemma foo: 0 <= n. Proof. -(* declaring an Axiom during a proof makes it immediatly +(* declaring an Axiom during a proof makes it immediately usable, juste as a full Definition. *) Axiom bar : n = 1. rewrite bar. diff --git a/test-suite/dune b/test-suite/dune index cd33319fa4..041c181d66 100644 --- a/test-suite/dune +++ b/test-suite/dune @@ -22,6 +22,7 @@ ../doc/stdlib/index-list.html.template ; For the changelog test ../config/coq_config.py + (source_tree doc/changelog) (package coq) ; For fake_ide (package coqide-server) diff --git a/test-suite/interactive/ParalITP_smallproofs.v b/test-suite/interactive/ParalITP_smallproofs.v index 0d75d52a31..d2e6794c0b 100644 --- a/test-suite/interactive/ParalITP_smallproofs.v +++ b/test-suite/interactive/ParalITP_smallproofs.v @@ -14,7 +14,7 @@ (* 02110-1301 USA *) -(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith developement but are rather useful. +(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith development but are rather useful. *) Require Export ZArith. @@ -84,7 +84,7 @@ End projection. (*###########################################################################*) -(* Declaring some realtions on natural numbers for stepl and stepr tactics. *) +(* Declaring some relations on natural numbers for stepl and stepr tactics. *) (*###########################################################################*) Lemma le_stepl: forall x y z, le x y -> x=z -> le z y. @@ -173,7 +173,7 @@ Qed. (*###########################################################################*) -(* Declaring some realtions on integers for stepl and stepr tactics. *) +(* Declaring some relations on integers for stepl and stepr tactics. *) (*###########################################################################*) Lemma Zle_stepl: forall x y z, (x<=y)%Z -> x=z -> (z<=y)%Z. diff --git a/test-suite/misc/changelog.sh b/test-suite/misc/changelog.sh index ed473e5874..76eb0de5aa 100755 --- a/test-suite/misc/changelog.sh +++ b/test-suite/misc/changelog.sh @@ -1,4 +1,4 @@ -#!/bin/sh +#!/usr/bin/env bash if grep -q -F "is_a_released_version = False" ../config/coq_config.py; then echo "This is not a released version: nothing to test." @@ -7,7 +7,8 @@ fi for d in ../doc/changelog/*; do if [ -d "$d" ]; then - if [ "$(ls $d/*.rst | wc -l)" != "1" ]; then + files=("$d"/*.rst) + if [ "${#files[@]}" != 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 diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index dcc8bd7165..29614c032a 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -209,7 +209,7 @@ Notation "'exists_mixed' x .. y , P" := (ex (fun x => forall z:nat, .. (ex (fun Check exists_mixed x y '(u,t), x+y=0/\u+t=0. Check exists_mixed x y '(z,t), x+y=0/\z+t=0. -(* Check that intermediary let-in are inserted inbetween instances of +(* Check that intermediary let-in are inserted in between instances of the repeated pattern *) Notation "'exists_true' x .. y , P" := (exists x, True /\ .. (exists y, True /\ P) ..) (at level 200, x binder). Check exists_true '(x,y) (u:=0) '(z,t), x+y=0/\z+t=0. diff --git a/test-suite/output/injection.out b/test-suite/output/injection.out new file mode 100644 index 0000000000..ff40a478f3 --- /dev/null +++ b/test-suite/output/injection.out @@ -0,0 +1,4 @@ +The command has indeed failed with message: +Unexpected pattern. +The command has indeed failed with message: +Unexpected injection pattern. diff --git a/test-suite/output/injection.v b/test-suite/output/injection.v new file mode 100644 index 0000000000..bfd5a67bf5 --- /dev/null +++ b/test-suite/output/injection.v @@ -0,0 +1,8 @@ +(* Test error messages *) + +Goal forall x, (x,0) = (0, S x) -> x = 0. +Fail intros x H; injection H as [= H'] H''. +Fail intros x H; injection H as H' [= H'']. +intros x H; injection H as [= H' H'']. +exact H'. +Qed. diff --git a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v index 3c427237b4..69ed621877 100644 --- a/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v +++ b/test-suite/stm/Nijmegen_QArithSternBrocot_Zaux.v @@ -14,7 +14,7 @@ (* 02110-1301 USA *) -(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith developement but are rather useful. +(** This file includes random facts about Integers (and natural numbers) which are not found in the standard library. Some of the lemma here are not used in the QArith development but are rather useful. *) Require Export ZArith. @@ -84,7 +84,7 @@ End projection. (*###########################################################################*) -(* Declaring some realtions on natural numbers for stepl and stepr tactics. *) +(* Declaring some relations on natural numbers for stepl and stepr tactics. *) (*###########################################################################*) Lemma le_stepl: forall x y z, le x y -> x=z -> le z y. @@ -173,7 +173,7 @@ Qed. (*###########################################################################*) -(* Declaring some realtions on integers for stepl and stepr tactics. *) +(* Declaring some relations on integers for stepl and stepr tactics. *) (*###########################################################################*) Lemma Zle_stepl: forall x y z, (x<=y)%Z -> x=z -> (z<=y)%Z. diff --git a/test-suite/success/Case15.v b/test-suite/success/Case15.v index 69fca48e24..ba6bf3bba2 100644 --- a/test-suite/success/Case15.v +++ b/test-suite/success/Case15.v @@ -20,7 +20,7 @@ Definition test (B : Boite) := | boite false (n, m) => n + m end. -(* Check lazyness of compilation ... future work +(* Check laziness of compilation ... future work Inductive I : Set := c : (b:bool)(if b then bool else nat)->I. Check [x] diff --git a/test-suite/success/Case18.v b/test-suite/success/Case18.v index be9ca8d41b..6bea435090 100644 --- a/test-suite/success/Case18.v +++ b/test-suite/success/Case18.v @@ -1,7 +1,10 @@ (* Check or-patterns *) +(* Non-interference with Numbers divisibility. *) +Reserved Notation "( p | q )" (at level 0). + Definition g x := - match x with ((((1 as x),_) | (_,x)), (_,(2 as y))|(y,_)) => (x,y) end. + match x with ((((1 as x),_) | (_,x)), ((_,(2 as y)) | (y,_))) => (x,y) end. Check (refl_equal _ : g ((1,2),(3,4)) = (1,3)). diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v index 8d9edbd62d..02e15b8ee2 100644 --- a/test-suite/success/CasesDep.v +++ b/test-suite/success/CasesDep.v @@ -62,7 +62,7 @@ Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option n (* -------------------------------------------------------------------- *) (* Example to test patterns matching on dependent families *) -(* This exemple extracted from the developement done by Nacira Chabane *) +(* This exemple extracted from the development done by Nacira Chabane *) (* (equipe Paris 6) *) (* -------------------------------------------------------------------- *) @@ -298,7 +298,7 @@ End Version1. (* ------------------------------------------------------------------*) -(* Initial exemple (without patterns) *) +(* Initial example (without patterns) *) (*-------------------------------------------------------------------*) Module Version2. diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v index 2f13b7c225..e96a5f9048 100644 --- a/test-suite/success/Hints.v +++ b/test-suite/success/Hints.v @@ -175,7 +175,7 @@ End HintCut. (* Check that auto-like tactics do not prefer "eq_refl" over more complex solutions, *) -(* e.g. those tactics when considering a goal with existential varibles *) +(* e.g. those tactics when considering a goal with existential variables *) (* like "m = ?n" won't pick "plus_n_O" hint over "eq_refl" hint. *) (* See this Coq club post for more detail: *) (* https://sympa.inria.fr/sympa/arc/coq-club/2017-12/msg00103.html *) diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v index ee540d7109..1dbeaf3e1f 100644 --- a/test-suite/success/Inversion.v +++ b/test-suite/success/Inversion.v @@ -179,7 +179,7 @@ exact Logic.I. Qed. (* Up to September 2014, H0 below was renamed called H1 because of a collision - with the automaticallly generated names for equations. + with the automatically generated names for equations. (example taken from CoLoR) *) Inductive term := Var | Fun : term -> term -> term. diff --git a/test-suite/success/Reordering.v b/test-suite/success/Reordering.v index de9b997590..98759264e5 100644 --- a/test-suite/success/Reordering.v +++ b/test-suite/success/Reordering.v @@ -1,7 +1,7 @@ (* Testing the reordering of hypothesis required by pattern, fold and change. *) Goal forall (A:Set) (x:A) (A':=A), True. intros. -fold A' in x. (* suceeds: x is moved after A' *) +fold A' in x. (* succeeds: x is moved after A' *) Undo. pattern A' in x. Undo. diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v index fb0adabae9..c566a6db9f 100644 --- a/test-suite/success/extraction_dep.v +++ b/test-suite/success/extraction_dep.v @@ -34,7 +34,7 @@ Definition testAbis := Abis.u + Abis.y. Recursive Extraction testAbis. (* without: A B v w x *) Extraction TestCompile testAbis. -(** 2) With signature, we only keep elements mentionned in signature. *) +(** 2) With signature, we only keep elements mentioned in signature. *) Module Type SIG. Parameter u : nat. diff --git a/test-suite/success/if.v b/test-suite/success/if.v index c81d2b9bf1..68d26ac8df 100644 --- a/test-suite/success/if.v +++ b/test-suite/success/if.v @@ -1,4 +1,4 @@ -(* The synthesis of the elimination predicate may fail if algebric *) +(* The synthesis of the elimination predicate may fail if algebraic *) (* universes are not cautiously treated *) Check (fun b : bool => if b then Type else nat). diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v index ddbc128aa1..6a4a0445b5 100644 --- a/theories/Arith/Peano_dec.v +++ b/theories/Arith/Peano_dec.v @@ -53,7 +53,7 @@ destruct le_mn1; intros le_mn2; destruct le_mn2. now destruct (Nat.nle_succ_diag_l _ le_mn0). + intros def_n0; generalize le_mn1; rewrite def_n0; intros le_mn0. now destruct (Nat.nle_succ_diag_l _ le_mn0). -+ intros def_n0. injection def_n0 as ->. ++ intros def_n0. injection def_n0 as [= ->]. rewrite (UIP_nat _ _ def_n0 eq_refl); simpl. assert (H : le_mn1 = le_mn2). now apply IHn0. diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 7f26181108..8abd4a3cbb 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -76,7 +76,7 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). (** Decidable leibniz equality instances. *) -(** The equiv is burried inside the setoid, but we can recover it by specifying +(** The equiv is buried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) Program Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index f6b240bf20..28394b984e 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -77,7 +77,7 @@ Infix "<>b" := nequiv_decb (no associativity, at level 70). Require Import Coq.Arith.Arith. -(** The equiv is burried inside the setoid, but we can recover +(** The equiv is buried inside the setoid, but we can recover it by specifying which setoid we're talking about. *) Program Instance eq_setoid A : Setoid A | 10 := diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index e68bc5930d..153842654a 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -1988,7 +1988,7 @@ Module OrdProperties (M:S). simpl; intros; try discriminate. intros. destruct a; destruct l; simpl in *. - injection H as -> ->. + injection H as [= -> ->]. inversion_clear H1. red in H; simpl in *; intuition. elim H0; eauto. @@ -2052,7 +2052,7 @@ Module OrdProperties (M:S). generalize (elements_3 m). destruct (elements m). try discriminate. - destruct p; injection H as -> ->; intros H4. + destruct p; injection H as [= -> ->]; intros H4. inversion_clear H1 as [? ? H2|? ? H2]. red in H2; destruct H2; simpl in *; ME.order. inversion_clear H4. rename H1 into H3. diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v index 8970529103..a12e4a43c2 100644 --- a/theories/FSets/FMapInterface.v +++ b/theories/FSets/FMapInterface.v @@ -192,7 +192,7 @@ Module Type WSfun (E : DecidableType). (** Equality of maps *) (** Caveat: there are at least three distinct equality predicates on maps. - - The simpliest (and maybe most natural) way is to consider keys up to + - The simplest (and maybe most natural) way is to consider keys up to their equivalence [E.eq], but elements up to Leibniz equality, in the spirit of [eq_key_elt] above. This leads to predicate [Equal]. - Unfortunately, this [Equal] predicate can't be used to describe diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index b47c99244b..37dd2304da 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -277,7 +277,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. rewrite append_assoc_1; apply in_or_app; right; apply in_cons; apply IHm2; auto. rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. - rewrite append_neutral_r; apply in_or_app; injection H as ->; + rewrite append_neutral_r; apply in_or_app; injection H as [= ->]; right; apply in_eq. rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto. rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto. @@ -318,7 +318,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. apply in_or_app. left; apply IHm1; auto. right; destruct (in_inv H0). - injection H1 as -> ->; apply in_eq. + injection H1 as [= -> ->]; apply in_eq. apply in_cons; apply IHm2; auto. left; apply IHm1; auto. right; apply IHm2; auto. @@ -349,7 +349,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. apply in_or_app. left; apply IHm1; auto. right; destruct (in_inv H0). - injection H1 as -> ->; apply in_eq. + injection H1 as [= -> ->]; apply in_eq. apply in_cons; apply IHm2; auto. left; apply IHm1; auto. right; apply IHm2; auto. @@ -692,7 +692,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst. red; red; simpl. destruct H0. - injection H0 as H0 _; subst. + injection H0 as [= H0 _]; subst. eapply xelements_bits_lt_1; eauto. apply E.bits_lt_trans with p. eapply xelements_bits_lt_1; eauto. diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v index 83bb07ffb6..d977ac05ec 100644 --- a/theories/FSets/FSetDecide.v +++ b/theories/FSets/FSetDecide.v @@ -240,7 +240,7 @@ the above form: True. Proof. intros. push not in *. - (* note that ~(R->P) remains (since R isnt decidable) *) + (* note that ~(R->P) remains (since R isn't decidable) *) tauto. Qed. diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v index 8a93f38164..d2e10e42a6 100644 --- a/theories/FSets/FSetPositive.v +++ b/theories/FSets/FSetPositive.v @@ -1009,10 +1009,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct o. intros x H. injection H; intros; subst. reflexivity. revert IHl. case choose. - intros p Hp x H. injection H as <-. apply Hp. + intros p Hp x [= <-]. apply Hp. reflexivity. intros _ x. revert IHr. case choose. - intros p Hp H. injection H as <-. apply Hp. + intros p Hp [= <-]. apply Hp. reflexivity. intros. discriminate. Qed. @@ -1068,11 +1068,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (min_elt l); intros. - injection H as <-. apply IHl. reflexivity. + injection H as [= <-]. apply IHl. reflexivity. destruct o; simpl. - injection H as <-. reflexivity. + injection H as [= <-]. reflexivity. destruct (min_elt r); simpl in *. - injection H as <-. apply IHr. reflexivity. + injection H as [= <-]. apply IHr. reflexivity. discriminate. Qed. @@ -1096,15 +1096,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (min_elt l). - intros p Hp. rewrite Hp in H. injection H as <-. + intros p Hp. rewrite Hp in H. injection H as [= <-]. destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial. intro Hp; rewrite Hp in H. apply min_elt_3 in Hp. destruct o. - injection H as <-. intros Hl. + injection H as [= <-]. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (min_elt r). - injection H as <-. + injection H as [= <-]. destruct y as [z|z|]. apply (IHr e z); trivial. elim (Hp _ H'). @@ -1121,11 +1121,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (max_elt r); intros. - injection H as <-. apply IHr. reflexivity. + injection H as [= <-]. apply IHr. reflexivity. destruct o; simpl. - injection H as <-. reflexivity. + injection H as [= <-]. reflexivity. destruct (max_elt l); simpl in *. - injection H as <-. apply IHl. reflexivity. + injection H as [= <-]. apply IHl. reflexivity. discriminate. Qed. @@ -1149,15 +1149,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (max_elt r). - intros p Hp. rewrite Hp in H. injection H as <-. + intros p Hp. rewrite Hp in H. injection H as [= <-]. destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial. intro Hp; rewrite Hp in H. apply max_elt_3 in Hp. destruct o. - injection H as <-. intros Hl. + injection H as [= <-]. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (max_elt l). - injection H as <-. + injection H as [= <-]. destruct y as [z|z|]. elim (Hp _ H'). apply (IHl e z); trivial. diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v index 1a391ed799..d54c8bf42d 100644 --- a/theories/Init/Logic.v +++ b/theories/Init/Logic.v @@ -37,7 +37,7 @@ Notation "~ x" := (not x) : type_scope. Register not as core.not.type. (** Create the "core" hint database, and set its transparent state for - variables and constants explicitely. *) + variables and constants explicitly. *) Create HintDb core. Hint Variables Opaque : core. diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v index 7e7a1ced58..5952f3a31b 100644 --- a/theories/Init/Nat.v +++ b/theories/Init/Nat.v @@ -331,7 +331,7 @@ Definition iter (n:nat) {A} (f:A->A) (x:A) : A := (** Bitwise operations *) (** We provide here some bitwise operations for unary numbers. - Some might be really naive, they are just there for fullfiling + Some might be really naive, they are just there for fulfilling the same interface as other for natural representations. As soon as binary representations such as NArith are available, it is clearly better to convert to/from them and use their ops. diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v index 497cf2550b..7eb717787e 100644 --- a/theories/Init/Tactics.v +++ b/theories/Init/Tactics.v @@ -75,7 +75,7 @@ Ltac case_eq x := generalize (eq_refl x); pattern x at -1; case x. (* use either discriminate or injection on a hypothesis *) -Ltac destr_eq H := discriminate H || (try (injection H as H)). +Ltac destr_eq H := discriminate H || (try (injection H as [= H])). (* Similar variants of destruct *) diff --git a/theories/Lists/List.v b/theories/Lists/List.v index a48e9929c4..f73440eb1a 100644 --- a/theories/Lists/List.v +++ b/theories/Lists/List.v @@ -250,7 +250,7 @@ Section Facts. generalize (app_nil_r l); intros E. rewrite -> E; auto. intros. - injection H as H H0. + injection H as [= H H0]. assert ([] = l ++ a0 :: l0) by auto. apply app_cons_not_nil in H1 as []. Qed. @@ -261,18 +261,14 @@ Section Facts. induction x as [| x l IHl]; [ destruct y as [| a l] | destruct y as [| a l0] ]; simpl; auto. - - intros a b H. - injection H. + - intros a b [= ]. auto. - - intros a0 b H. - injection H as H1 H0. + - intros a0 b [= H1 H0]. apply app_cons_not_nil in H0 as []. - - intros a b H. - injection H as H1 H0. + - intros a b [= H1 H0]. assert ([] = l ++ [a]) by auto. apply app_cons_not_nil in H as []. - - intros a0 b H. - injection H as <- H0. + - intros a0 b [= <- H0]. destruct (IHl l0 a0 b H0) as (<-,<-). split; auto. Qed. @@ -336,7 +332,7 @@ Section Facts. absurd (length (x1 :: l1 ++ l) <= length l). simpl; rewrite app_length; auto with arith. rewrite H; auto with arith. - injection H as H H0; f_equal; eauto. + injection H as [= H H0]; f_equal; eauto. Qed. End Facts. @@ -519,7 +515,7 @@ Section Elts. Proof. revert l. induction n as [|n IH]; intros [|x l] H; simpl in *; try easy. - - exists nil; exists l. now injection H as ->. + - exists nil; exists l. now injection H as [= ->]. - destruct (IH _ H) as (l1 & l2 & H1 & H2). exists (x::l1); exists l2; simpl; split; now f_equal. Qed. @@ -1243,7 +1239,7 @@ End Fold_Right_Recursor. Proof. induction l as [|a l IH]; simpl; [easy| ]. case_eq (f a); intros Ha Eq. - * injection Eq as ->; auto. + * injection Eq as [= ->]; auto. * destruct (IH Eq); auto. Qed. @@ -1304,10 +1300,10 @@ End Fold_Right_Recursor. forall x:A, In x l <-> In x l1 \/ In x l2. Proof. revert l1 l2. induction l as [| a l' Hrec]; simpl; intros l1 l2 Eq x. - - injection Eq as <- <-. tauto. + - injection Eq as [= <- <-]. tauto. - destruct (partition l') as (left, right). specialize (Hrec left right eq_refl x). - destruct (f a); injection Eq as <- <-; simpl; tauto. + destruct (f a); injection Eq as [= <- <-]; simpl; tauto. Qed. End Bool. @@ -1483,7 +1479,7 @@ End Fold_Right_Recursor. destruct (in_app_or _ _ _ H); clear H. destruct (in_map_iff (fun y : B => (a, y)) l' (x,y)) as (H1,_). destruct (H1 H0) as (z,(H2,H3)); clear H0 H1. - injection H2 as -> ->; intuition. + injection H2 as [= -> ->]; intuition. intuition. Qed. diff --git a/theories/Lists/StreamMemo.v b/theories/Lists/StreamMemo.v index 419a0be49c..e1e0d3db4c 100644 --- a/theories/Lists/StreamMemo.v +++ b/theories/Lists/StreamMemo.v @@ -70,7 +70,7 @@ Qed. End MemoFunction. (** For a dependent function, the previous solution is - reused thanks to a temporarly hiding of the dependency + reused thanks to a temporary hiding of the dependency in a "container" [memo_val]. *) Section DependentMemoFunction. diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v index b06384e992..73d7432193 100644 --- a/theories/Logic/ClassicalFacts.v +++ b/theories/Logic/ClassicalFacts.v @@ -385,7 +385,7 @@ End Proof_irrelevance_EM_CC. fragment of [Prop] into [bool], hence weak classical logic, i.e. [forall A, ~A\/~~A], is enough for deriving a weak version of proof-irrelevance. This is enough to derive a contradiction from a - [Set]-bound weak excluded middle wih an impredicative [Set] + [Set]-bound weak excluded middle with an impredicative [Set] universe. *) Section Proof_irrelevance_WEM_CC. diff --git a/theories/Logic/WeakFan.v b/theories/Logic/WeakFan.v index c9822f47dc..13f63c5cbc 100644 --- a/theories/Logic/WeakFan.v +++ b/theories/Logic/WeakFan.v @@ -64,7 +64,7 @@ induction l1, l2. - discriminate. - discriminate. - intros H (HY1,H1) (HY2,H2). - injection H as H. + injection H as [= H]. pose proof (IHl1 l2 H HY1 HY2). clear HY1 HY2 H IHl1. subst l1. f_equal. diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v index f228cbb3bf..3ceff849be 100644 --- a/theories/MSets/MSetDecide.v +++ b/theories/MSets/MSetDecide.v @@ -240,7 +240,7 @@ the above form: True. Proof. intros. push not in *. - (* note that ~(R->P) remains (since R isnt decidable) *) + (* note that ~(R->P) remains (since R isn't decidable) *) tauto. Qed. diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v index a3dcca7dfd..838721f499 100644 --- a/theories/MSets/MSetGenTree.v +++ b/theories/MSets/MSetGenTree.v @@ -166,7 +166,7 @@ end. *) (** Enumeration of the elements of a tree. This corresponds - to the "samefringe" notion in the litterature. *) + to the "samefringe" notion in the literature. *) #[universes(template)] Inductive enumeration := diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v index 6a18f59fc4..85139593da 100644 --- a/theories/MSets/MSetInterface.v +++ b/theories/MSets/MSetInterface.v @@ -659,7 +659,7 @@ End Raw2Sets. (** It is in fact possible to provide an ordering on sets with very little information on them (more or less only the [In] predicate). This generic build of ordering is in fact not - used for the moment, we rather use a simplier version + used for the moment, we rather use a simpler version dedicated to sets-as-sorted-lists, see [MakeListOrdering]. *) diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v index a726eebd31..330c7959ac 100644 --- a/theories/MSets/MSetPositive.v +++ b/theories/MSets/MSetPositive.v @@ -910,10 +910,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. destruct o. intros x H. injection H; intros; subst. reflexivity. revert IHl. case choose. - intros p Hp x H. injection H as <-. apply Hp. + intros p Hp x [= <-]. apply Hp. reflexivity. intros _ x. revert IHr. case choose. - intros p Hp H. injection H as <-. apply Hp. + intros p Hp [= <-]. apply Hp. reflexivity. intros. discriminate. Qed. @@ -970,11 +970,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (min_elt l); intros. - injection H as <-. apply IHl. reflexivity. + injection H as [= <-]. apply IHl. reflexivity. destruct o; simpl. - injection H as <-. reflexivity. + injection H as [= <-]. reflexivity. destruct (min_elt r); simpl in *. - injection H as <-. apply IHr. reflexivity. + injection H as [= <-]. apply IHr. reflexivity. discriminate. Qed. @@ -998,15 +998,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (min_elt l). - intros p Hp. rewrite Hp in H. injection H as <-. + intros p Hp. rewrite Hp in H. injection H as [= <-]. destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial. intro Hp; rewrite Hp in H. apply min_elt_spec3 in Hp. destruct o. - injection H as <-. intros Hl. + injection H as [= <-]. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (min_elt r). - injection H as <-. + injection H as [= <-]. destruct y as [z|z|]. apply (IHr e z); trivial. elim (Hp _ H'). @@ -1023,11 +1023,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [| l IHl o r IHr]; simpl. intros. discriminate. intros x. destruct (max_elt r); intros. - injection H as <-. apply IHr. reflexivity. + injection H as [= <-]. apply IHr. reflexivity. destruct o; simpl. - injection H as <-. reflexivity. + injection H as [= <-]. reflexivity. destruct (max_elt l); simpl in *. - injection H as <-. apply IHl. reflexivity. + injection H as [= <-]. apply IHl. reflexivity. discriminate. Qed. @@ -1051,15 +1051,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits. induction s as [|l IHl o r IHr]; intros x y H H'. discriminate. simpl in H. case_eq (max_elt r). - intros p Hp. rewrite Hp in H. injection H as <-. + intros p Hp. rewrite Hp in H. injection H as [= <-]. destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial. intro Hp; rewrite Hp in H. apply max_elt_spec3 in Hp. destruct o. - injection H as <-. intros Hl. + injection H as [= <-]. intros Hl. destruct y as [z|z|]; simpl; trivial. elim (Hp _ H'). destruct (max_elt l). - injection H as <-. + injection H as [= <-]. destruct y as [z|z|]. elim (Hp _ H'). apply (IHl e z); trivial. diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v index f9105fdf74..a2ffd2050e 100644 --- a/theories/MSets/MSetRBT.v +++ b/theories/MSets/MSetRBT.v @@ -1950,7 +1950,7 @@ Module Make (X: Orders.OrderedType) <: generalize (fun x s' => @Raw.remove_min_spec1 s x s' Hs). set (P := Raw.remove_min_ok s). clearbody P. destruct (Raw.remove_min s) as [(x0,s0)|]; try easy. - intros H U. injection U as -> <-. simpl. + intros H [= -> <-]. simpl. destruct (H x s0); auto. subst; intuition. Qed. diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index be12fffaaf..3e5987127a 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -25,7 +25,7 @@ Module N. Definition t := N. -(** ** Nicer name [N.pos] for contructor [Npos] *) +(** ** Nicer name [N.pos] for constructor [Npos] *) Notation pos := Npos. diff --git a/theories/Numbers/AltBinNotations.v b/theories/Numbers/AltBinNotations.v index c7e3999691..6809154a33 100644 --- a/theories/Numbers/AltBinNotations.v +++ b/theories/Numbers/AltBinNotations.v @@ -18,7 +18,7 @@ thousands of digits and more, conversion from/to [Decimal.int] can become significantly slow. If that becomes a problem for your development, this file provides some alternative [Numeral - Notation] commmands that use [Z] as bridge type. To enable these + Notation] commands that use [Z] as bridge type. To enable these commands, just be sure to [Require] this file after other files defining numeral notations. diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index 4b0bda3d44..a7bc4211ed 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -1288,7 +1288,7 @@ Section Int31_Specs. intros; rewrite <- spec_1; apply spec_add. Qed. - (** Substraction *) + (** Subtraction *) Lemma spec_sub_c : forall x y, [-|sub31c x y|] = [|x|] - [|y|]. Proof. diff --git a/theories/Numbers/Cyclic/Int31/Int31.v b/theories/Numbers/Cyclic/Int31/Int31.v index b9185c9ca0..10f819b005 100644 --- a/theories/Numbers/Cyclic/Int31/Int31.v +++ b/theories/Numbers/Cyclic/Int31/Int31.v @@ -255,7 +255,7 @@ Definition add31carryc (n m : int31) := | _ => C1 npmpone end. -(** * Substraction *) +(** * Subtraction *) (** Subtraction modulo [2^31] *) diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v index 4bcd22543f..94da55b3f3 100644 --- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v +++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v @@ -372,7 +372,7 @@ Section ZModulo. assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)). unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l). - destruct 1; injection H as ? ?. + destruct 1; injection H as [= ? ?]. rewrite H0. assert ([|l|] = l). apply Zmod_small; auto. @@ -414,7 +414,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod [|a|] [|b|] H0). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H1 as ? ?. + injection H1 as [= ? ?]. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. @@ -525,7 +525,7 @@ Section ZModulo. unfold Z.modulo, Z.div; destruct Z.div_eucl; auto. generalize (Z_div_mod a [|b|] H3). destruct Z.div_eucl as (q,r); destruct 1; intros. - injection H4 as ? ?. + injection H4 as [= ? ?]. assert ([|r|]=r). apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|]; auto with zarith. diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index 4aabda77ee..42ea8f76fb 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -324,7 +324,7 @@ Proof. now rewrite <- opp_succ, opp_nonneg_nonpos, le_succ_l. Qed. -(** Accesing a high enough bit of a number gives its sign *) +(** Accessing a high enough bit of a number gives its sign *) Lemma bits_iff_nonneg : forall a n, log2 (abs a) < n -> (0<=a <-> a.[n] = false). diff --git a/theories/Numbers/Integer/Abstract/ZLcm.v b/theories/Numbers/Integer/Abstract/ZLcm.v index 0ab528de80..377c05e279 100644 --- a/theories/Numbers/Integer/Abstract/ZLcm.v +++ b/theories/Numbers/Integer/Abstract/ZLcm.v @@ -207,7 +207,7 @@ Qed. We had an abs in order to have an always-nonnegative lcm, in the spirit of gcd. Nota: [lcm 0 0] should be 0, which - isn't garantee with the third equation above. + isn't guarantee with the third equation above. *) Definition lcm a b := abs (a*(b/gcd a b)). diff --git a/theories/Numbers/NatInt/NZAddOrder.v b/theories/Numbers/NatInt/NZAddOrder.v index 5f102e853b..b96a2b35af 100644 --- a/theories/Numbers/NatInt/NZAddOrder.v +++ b/theories/Numbers/NatInt/NZAddOrder.v @@ -149,7 +149,7 @@ Proof. intros n m H; apply add_le_cases; now nzsimpl. Qed. -(** Substraction *) +(** Subtraction *) (** We can prove the existence of a subtraction of any number by a smaller one *) diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v index acebfcf1d2..cace65c61d 100644 --- a/theories/Numbers/NatInt/NZDomain.v +++ b/theories/Numbers/NatInt/NZDomain.v @@ -310,7 +310,7 @@ Qed. End NZOfNatOrd. -(** For basic operations, we can prove correspondance with +(** For basic operations, we can prove correspondence with their counterpart in [nat]. *) Module NZOfNatOps (Import NZ:NZAxiomsSig'). diff --git a/theories/Numbers/Natural/Abstract/NLcm.v b/theories/Numbers/Natural/Abstract/NLcm.v index 47b74193ed..19a8b4b2b1 100644 --- a/theories/Numbers/Natural/Abstract/NLcm.v +++ b/theories/Numbers/Natural/Abstract/NLcm.v @@ -90,7 +90,7 @@ Qed. = (a / gcd a b) * b = (a*b) / gcd a b - Nota: [lcm 0 0] should be 0, which isn't garantee with the third + Nota: [lcm 0 0] should be 0, which isn't guarantee with the third equation above. *) diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 7f30733559..1c78011941 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -310,7 +310,7 @@ Infix "<?" := ltb (at level 70, no associativity) : positive_scope. (** ** A Square Root function for positive numbers *) -(** We procede by blocks of two digits : if p is written qbb' +(** We proceed by blocks of two digits : if p is written qbb' then sqrt(p) will be sqrt(q)~0 or sqrt(q)~1. For deciding easily in which case we are, we store the remainder (as a mask, since it can be null). diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 5ae933d433..9fe3b967ae 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -31,7 +31,7 @@ Definition block {A : Type} (a : A) := a. Ltac block_goal := match goal with [ |- ?T ] => change (block T) end. Ltac unblock_goal := unfold block in *. -(** Notation for heterogenous equality. *) +(** Notation for heterogeneous equality. *) Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity). @@ -88,7 +88,7 @@ Ltac elim_eq_rect := end end. -(** Rewrite using uniqueness of indentity proofs [H = eq_refl]. *) +(** Rewrite using uniqueness of identity proofs [H = eq_refl]. *) Ltac simpl_uip := match goal with @@ -450,7 +450,7 @@ Tactic Notation "dependent" "destruction" ident(H) "generalizing" ne_hyp_list(l) do_depelim' ltac:(fun hyp => revert l) ltac:(fun hyp => destruct hyp using c) H. (** Then we have wrappers for usual calls to induction. One can customize the induction tactic by - writting another wrapper calling do_depelim. We suppose the hyp has to be generalized before + writing another wrapper calling do_depelim. We suppose the hyp has to be generalized before calling [induction]. *) Tactic Notation "dependent" "induction" ident(H) := diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v index f18fca99a0..9eae960086 100644 --- a/theories/QArith/Qcanon.v +++ b/theories/QArith/Qcanon.v @@ -43,10 +43,10 @@ Proof. generalize (Z.gcd_nonneg a (Zpos b)) (Z.ggcd_correct_divisors a (Zpos b)). rewrite <- Z.ggcd_gcd. destruct Z.ggcd as (g,(aa,bb)); simpl in *. - injection H as <- <-. intros H (_,H'). + injection H as [= <- <-]. intros H (_,H'). destruct g as [|g|g]; [ discriminate | | now elim H ]. destruct bb as [|b|b]; simpl in *; try discriminate. - injection H' as H'. f_equal. + injection H' as [= H']. f_equal. apply Pos.mul_reg_r with b. now rewrite Pos.mul_1_l. Qed. @@ -87,7 +87,7 @@ Arguments Q2Qc q%Q. Lemma Q2Qc_eq_iff (q q' : Q) : Q2Qc q = Q2Qc q' <-> q == q'. Proof. split; intro H. - - now injection H as H%Qred_eq_iff. + - now injection H as [= H%Qred_eq_iff]. - apply Qc_is_canon. simpl. now rewrite H. Qed. @@ -269,7 +269,7 @@ Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0. Proof. intros. destruct (Qmult_integral x y); try qc; auto. - injection H as H. + injection H as [= H]. rewrite <- (Qred_correct (x*y)). rewrite <- (Qred_correct 0). rewrite H; auto with qarith. diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v index ec283b886e..45cd74cf48 100644 --- a/theories/Reals/RIneq.v +++ b/theories/Reals/RIneq.v @@ -95,7 +95,7 @@ Proof. Qed. (*********************************************************) -(** ** Relating [<], [>], [<=] and [>=] *) +(** ** Relating [<], [>], [<=] and [>=] *) (*********************************************************) (*********************************************************) @@ -711,7 +711,7 @@ Proof. Qed. (*********************************************************) -(** ** Subtraction *) +(** ** Subtraction *) (*********************************************************) Lemma Rminus_0_r : forall r, r - 0 = r. @@ -1352,7 +1352,7 @@ Proof. Qed. (*********************************************************) -(** ** Order and substraction *) +(** ** Order and subtraction *) (*********************************************************) Lemma Rlt_minus : forall r1 r2, r1 < r2 -> r1 - r2 < 0. diff --git a/theories/Sorting/PermutSetoid.v b/theories/Sorting/PermutSetoid.v index 08bc400f0a..142883a525 100644 --- a/theories/Sorting/PermutSetoid.v +++ b/theories/Sorting/PermutSetoid.v @@ -543,7 +543,7 @@ Qed. End Permut_permut. (* begin hide *) -(** For compatibilty *) +(** For compatibility *) Notation permut_right := permut_cons (only parsing). Notation permut_tran := permut_trans (only parsing). (* end hide *) diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v index f5bc9eee4e..170c221a45 100644 --- a/theories/Sorting/Permutation.v +++ b/theories/Sorting/Permutation.v @@ -304,7 +304,7 @@ Qed. Lemma Permutation_length_1_inv: forall a l, Permutation [a] l -> l = [a]. Proof. intros a l H; remember [a] as m in H. - induction H; try (injection Heqm as -> ->); + induction H; try (injection Heqm as [= -> ->]); discriminate || auto. apply Permutation_nil in H as ->; trivial. Qed. @@ -312,7 +312,7 @@ Qed. Lemma Permutation_length_1: forall a b, Permutation [a] [b] -> a = b. Proof. intros a b H. - apply Permutation_length_1_inv in H; injection H as ->; trivial. + apply Permutation_length_1_inv in H; injection H as [= ->]; trivial. Qed. Lemma Permutation_length_2_inv : @@ -320,7 +320,7 @@ Lemma Permutation_length_2_inv : Proof. intros a1 a2 l H; remember [a1;a2] as m in H. revert a1 a2 Heqm. - induction H; intros; try (injection Heqm as ? ?; subst); + induction H; intros; try (injection Heqm as [= ? ?]; subst); discriminate || (try tauto). apply Permutation_length_1_inv in H as ->; left; auto. apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as []; @@ -332,7 +332,7 @@ Lemma Permutation_length_2 : a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1. Proof. intros a1 b1 a2 b2 H. - apply Permutation_length_2_inv in H as [H|H]; injection H as -> ->; auto. + apply Permutation_length_2_inv in H as [H|H]; injection H as [= -> ->]; auto. Qed. Lemma NoDup_Permutation l l' : NoDup l -> NoDup l' -> diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 08ccfac877..85bde6a4df 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -123,7 +123,7 @@ intros H; generalize (H O); simpl; intros H1; inversion H1. case (Rec s). intros H0; rewrite H0; auto. intros n; exact (H (S n)). -intros H; injection H as H1 H2. +intros [= H1 H2]. rewrite H2; trivial. rewrite H1; auto. Qed. @@ -290,14 +290,14 @@ intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl; auto. intros n; case n; simpl; auto. intros m s1; case s1; simpl; auto. -intros H; injection H as <-; auto. +intros [= <-]; auto. intros; discriminate. intros; discriminate. intros b s2' Rec n m s1. case n; simpl; auto. generalize (prefix_correct s1 (String b s2')); case (prefix s1 (String b s2')). -intros H0 H; injection H as <-; auto. +intros H0 [= <-]; auto. case H0; simpl; auto. case m; simpl; auto. case (index O s1 s2'); intros; discriminate. @@ -323,7 +323,7 @@ intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl; auto. intros n; case n; simpl; auto. intros m s1; case s1; simpl; auto. -intros H; injection H as <-. +intros [= <-]. intros p H0 H2; inversion H2. intros; discriminate. intros; discriminate. @@ -331,7 +331,7 @@ intros b s2' Rec n m s1. case n; simpl; auto. generalize (prefix_correct s1 (String b s2')); case (prefix s1 (String b s2')). -intros H0 H; injection H as <-; auto. +intros H0 [= <-]; auto. intros p H2 H3; inversion H3. case m; simpl; auto. case (index 0 s1 s2'); intros; discriminate. diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v index d000b75bf4..e5b2e22dc1 100644 --- a/theories/Structures/OrderedType.v +++ b/theories/Structures/OrderedType.v @@ -208,7 +208,7 @@ Module OrderedTypeFacts (Import O: OrderedType). unfold eqb; intros; destruct (eq_dec x y); elim_comp; auto. Qed. -(* Specialization of resuts about lists modulo. *) +(* Specialization of results about lists modulo. *) Section ForNotations. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 182b781fe1..354c1eb9b0 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -431,7 +431,7 @@ Proof. apply eq_true_iff_eq. now rewrite negb_true_iff, ltb_lt, leb_gt. Qed. -(** Relation bewteen [compare] and the boolean comparisons *) +(** Relation between [compare] and the boolean comparisons *) Lemma eqb_compare x y : (x =? y) = match compare x y with Eq => true | _ => false end. diff --git a/theories/Structures/OrdersTac.v b/theories/Structures/OrdersTac.v index ebd8ee8fc2..80925ff058 100644 --- a/theories/Structures/OrdersTac.v +++ b/theories/Structures/OrdersTac.v @@ -51,7 +51,7 @@ Local Infix "+" := trans_ord. This used to be provided here via a [TotalOrder], but for technical reasons related to extraction, we now ask - for two sperate parts: relations in a [EqLtLe] + properties in + for two separate parts: relations in a [EqLtLe] + properties in [IsTotalOrder]. Note that [TotalOrder = EqLtLe <+ IsTotalOrder] *) diff --git a/theories/Vectors/Fin.v b/theories/Vectors/Fin.v index 4088843a1b..0b3e9b78f6 100644 --- a/theories/Vectors/Fin.v +++ b/theories/Vectors/Fin.v @@ -160,7 +160,7 @@ Qed. (** The p{^ th} element of [fin m] viewed as the p{^ th} element of [fin (n + m)] -Really really ineficient !!! *) +Really really inefficient !!! *) Definition L_R {m} n (p : t m) : t (n + m). Proof. induction n. diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v index b2d08186ea..60db536dce 100644 --- a/theories/Wellfounded/Lexicographic_Product.v +++ b/theories/Wellfounded/Lexicographic_Product.v @@ -46,11 +46,11 @@ Section WfLexicographic_Product. apply H2. auto with sets. - + injection H1 as <- _. - injection H3 as <- _; auto with sets. + + injection H1 as [= <- _]. + injection H3 as [= <- _]; auto with sets. - rewrite <- H1. - injection H3 as -> H3. + injection H3 as [= -> H3]. apply IHAcc0. elim inj_pair2 with A B x y' x0; assumption. Defined. diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index a346ab8ccb..43841920e5 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1259,7 +1259,7 @@ Proof. f_equal. now rewrite <- add_assoc, add_opp_diag_r, add_0_r. Qed. -(** * [testbit] in terms of comparision. *) +(** * [testbit] in terms of comparison. *) Lemma testbit_mod_pow2 a n i (H : 0 <= n) : testbit (a mod 2 ^ n) i = ((i <? n) && testbit a i)%bool. diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index 8cb62622db..a9a5f15f2e 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -28,7 +28,7 @@ Module Z. Definition t := Z. -(** ** Nicer names [Z.pos] and [Z.neg] for contructors *) +(** ** Nicer names [Z.pos] and [Z.neg] for constructors *) Notation pos := Zpos. Notation neg := Zneg. diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v index 0b0ed48d51..9cade75f08 100644 --- a/theories/ZArith/Int.v +++ b/theories/ZArith/Int.v @@ -13,7 +13,7 @@ (** We define a signature for an integer datatype based on [Z]. The goal is to allow a switch after extraction to ocaml's [big_int] or even [int] when finiteness isn't a problem - (typically : when mesuring the height of an AVL tree). + (typically : when measuring the height of an AVL tree). *) Require Import BinInt. diff --git a/theories/ZArith/Zquot.v b/theories/ZArith/Zquot.v index a619eb90ef..64431a9411 100644 --- a/theories/ZArith/Zquot.v +++ b/theories/ZArith/Zquot.v @@ -105,7 +105,7 @@ Proof. rewrite Z.rem_sign_nz; trivial. apply Z.square_nonneg. Qed. -(** This can also be said in a simplier way: *) +(** This can also be said in a simpler way: *) Theorem Zrem_sgn2 a b : 0 <= (Z.rem a b) * a. Proof. diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 2ec55d1bd0..d37d2bea94 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -171,7 +171,7 @@ DYNOBJ:=.cmxs DYNLIB:=.cmxs endif -# these variables are meant to be overriden if you want to add *extra* flags +# these variables are meant to be overridden if you want to add *extra* flags COQEXTRAFLAGS?= COQCHKEXTRAFLAGS?= COQDOCEXTRAFLAGS?= diff --git a/tools/coqdep.ml b/tools/coqdep.ml index 8823206252..c00fb71dba 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -454,7 +454,7 @@ let usage () = eprintf " -I dir : add (non recursively) dir to ocaml path\n"; eprintf " -R dir -as logname : add and import dir recursively to coq load path under logical name logname\n"; (* deprecate? *) eprintf " -R dir logname : add and import dir recursively to coq load path under logical name logname\n"; - eprintf " -Q dir logname : add (recusively) and open (non recursively) dir to coq load path under logical name logname\n"; + eprintf " -Q dir logname : add (recursively) and open (non recursively) dir to coq load path under logical name logname\n"; eprintf " -dumpgraph f : print a dot dependency graph in file 'f'\n"; eprintf " -dumpgraphbox f : print a dot dependency graph box in file 'f'\n"; eprintf " -exclude-dir dir : skip subdirectories named 'dir' during -R/-Q search\n"; diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index b703af934d..75667ae909 100644 --- a/tools/coqdoc/output.ml +++ b/tools/coqdoc/output.ml @@ -762,7 +762,7 @@ module Html = struct (* inference rules *) let inf_rule assumptions (_,_,midnm) conclusions = - (* this first function replaces any occurance of 3 or more spaces + (* this first function replaces any occurrence of 3 or more spaces in a row with " "s. We do this to the assumptions so that people can put multiple rules on a line with nice formatting *) let replace_spaces str = diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli index 00db2ad317..6449cd5b6f 100644 --- a/tools/coqdoc/tokens.mli +++ b/tools/coqdoc/tokens.mli @@ -57,7 +57,7 @@ val translate : string -> string option dictionary, "<>_h" is one word and gets translated *) -(* Warning: do not output anything on output channel inbetween a call +(* Warning: do not output anything on output channel in between a call to [output_tagged_*] and [flush_sublexer]!! *) type out_function = diff --git a/tools/coqwc.mll b/tools/coqwc.mll index f0f138740c..06b4ad5fd3 100644 --- a/tools/coqwc.mll +++ b/tools/coqwc.mll @@ -207,7 +207,7 @@ and string = parse | eof { 0 } (*s The following entry [read_header] is used to skip the possible header at - the beggining of files (unless option \texttt{-e} is specified). + the beginning of files (unless option \texttt{-e} is specified). It stops whenever it encounters an empty line or any character outside a comment. In this last case, it correctly resets the lexer position on that character (decreasing [lex_curr_pos] by 1). *) diff --git a/toplevel/ccompile.ml b/toplevel/ccompile.ml index 2f63410761..7748134146 100644 --- a/toplevel/ccompile.ml +++ b/toplevel/ccompile.ml @@ -225,7 +225,7 @@ let do_vio opts copts = process happens outside of the STM *) if copts.vio_files <> [] || copts.vio_tasks <> [] then let iload_path = build_load_path opts in - List.iter Mltop.add_coq_path iload_path; + List.iter Loadpath.add_coq_path iload_path; (* Vio compile pass *) if copts.vio_files <> [] then schedule_vio copts; diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index ec43dbb1d7..4ef31c73b7 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -46,8 +46,8 @@ type t = { load_rcfile : bool; rcfile : string option; - ml_includes : Mltop.coq_path list; - vo_includes : Mltop.coq_path list; + ml_includes : Loadpath.coq_path list; + vo_includes : Loadpath.coq_path list; vo_requires : (string * string option * bool option) list; (* None = No Import; Some false = Import; Some true = Export *) @@ -147,10 +147,10 @@ let default = { (* Functional arguments *) (******************************************************************************) let add_ml_include opts s = - Mltop.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes } + Loadpath.{ opts with ml_includes = {recursive = false; path_spec = MlPath s} :: opts.ml_includes } let add_vo_include opts unix_path coq_path implicit = - let open Mltop in + let open Loadpath in let coq_path = Libnames.dirpath_of_string coq_path in { opts with vo_includes = { recursive = true; @@ -273,7 +273,7 @@ let usage help = end; let lp = Coqinit.toplevel_init_load_path () in (* Necessary for finding the toplevels below *) - List.iter Mltop.add_coq_path lp; + List.iter Loadpath.add_coq_path lp; help () (* Main parsing routine *) diff --git a/toplevel/coqargs.mli b/toplevel/coqargs.mli index d7f9819bee..015789c1f3 100644 --- a/toplevel/coqargs.mli +++ b/toplevel/coqargs.mli @@ -22,8 +22,8 @@ type t = { load_rcfile : bool; rcfile : string option; - ml_includes : Mltop.coq_path list; - vo_includes : Mltop.coq_path list; + ml_includes : Loadpath.coq_path list; + vo_includes : Loadpath.coq_path list; vo_requires : (string * string option * bool option) list; toplevel_name : Stm.interactive_top; @@ -69,4 +69,4 @@ val parse_args : help:(unit -> unit) -> init:t -> string list -> t * string list val exitcode : t -> int val require_libs : t -> (string * string option * bool option) list -val build_load_path : t -> Mltop.coq_path list +val build_load_path : t -> Loadpath.coq_path list diff --git a/toplevel/coqcargs.ml b/toplevel/coqcargs.ml index 2279ce5505..63c37e2251 100644 --- a/toplevel/coqcargs.ml +++ b/toplevel/coqcargs.ml @@ -63,7 +63,10 @@ let check_compilation_output_name_consistency args = prerr_endline ("file have to be compiled") | _ -> () +let is_dash_argument s = String.length s > 0 && s.[0] = '-' + let add_compile ?echo copts s = + if is_dash_argument s then (prerr_endline ("Unknown option " ^ s); exit 1); (* make the file name explicit; needed not to break up Coq loadpath stuff. *) let echo = Option.default copts.echo echo in let s = diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index 74a089510e..f4ae00ed65 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -17,7 +17,7 @@ let set_debug () = let () = Backtrace.record_backtrace true in Flags.debug := true -(* Loading of the ressource file. +(* Loading of the resource file. rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one does not exist. *) @@ -53,25 +53,25 @@ let load_rcfile ~rcfile ~state = (* Recursively puts dir in the LoadPath if -nois was not passed *) let build_stdlib_path ~load_init ~unix_path ~coq_path ~with_ml = - let open Mltop in + let open Loadpath in let add_ml = if with_ml then AddRecML else AddNoML in { recursive = true; path_spec = VoPath { unix_path; coq_path ; has_ml = add_ml; implicit = load_init } } let build_userlib_path ~unix_path = - let open Mltop in + let open Loadpath in { recursive = true; path_spec = VoPath { unix_path; coq_path = Libnames.default_root_prefix; - has_ml = Mltop.AddRecML; + has_ml = AddRecML; implicit = false; } } let ml_path_if c p = - let open Mltop in + let open Loadpath in let f x = { recursive = false; path_spec = MlPath x } in if c then List.map f p else [] @@ -85,7 +85,7 @@ let toplevel_init_load_path () = (* LoadPath for Coq user libraries *) let libs_init_load_path ~load_init = - let open Mltop in + let open Loadpath in let coqlib = Envars.coqlib () in let user_contrib = coqlib/"user-contrib" in let xdg_dirs = Envars.xdg_dirs ~warn:(fun x -> Feedback.msg_warning (str x)) in @@ -115,10 +115,10 @@ let libs_init_load_path ~load_init = (* Initialises the Ocaml toplevel before launching it, so that it can find the "include" file in the *source* directory *) let init_ocaml_path () = - let open Mltop in + let open Loadpath in let lp s = { recursive = false; path_spec = MlPath s } in let add_subdir dl = - Mltop.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl])) + Loadpath.add_coq_path (lp (List.fold_left (/) Envars.coqroot [dl])) in - Mltop.add_coq_path (lp (Envars.coqlib ())); + Loadpath.add_coq_path (lp (Envars.coqlib ())); List.iter add_subdir Coq_config.all_src_dirs diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli index c891e736b4..04ec77a025 100644 --- a/toplevel/coqinit.mli +++ b/toplevel/coqinit.mli @@ -17,7 +17,7 @@ val load_rcfile : rcfile:(string option) -> state:Vernac.State.t -> Vernac.State val init_ocaml_path : unit -> unit (* LoadPath for toploop toplevels *) -val toplevel_init_load_path : unit -> Mltop.coq_path list +val toplevel_init_load_path : unit -> Loadpath.coq_path list (* LoadPath for Coq user libraries *) -val libs_init_load_path : load_init:bool -> Mltop.coq_path list +val libs_init_load_path : load_init:bool -> Loadpath.coq_path list diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli index 0cc22ba31d..852a65f07b 100644 --- a/toplevel/coqloop.mli +++ b/toplevel/coqloop.mli @@ -17,7 +17,7 @@ type input_buffer = { mutable prompt : Stm.doc -> string; mutable str : Bytes.t; (** buffer of already read characters *) mutable len : int; (** number of chars in the buffer *) - mutable bols : int list; (** offsets in str of begining of lines *) + mutable bols : int list; (** offsets in str of beginning of lines *) mutable tokens : Pcoq.Parsable.t; (** stream of tokens *) mutable start : int } (** stream count of the first char of the buffer *) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index b769405cf6..460c2f126e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -222,7 +222,7 @@ let init_toplevel ~help ~init custom_init arglist = exit 0; end; let top_lp = Coqinit.toplevel_init_load_path () in - List.iter Mltop.add_coq_path top_lp; + List.iter Loadpath.add_coq_path top_lp; let opts, extras = custom_init ~opts extras in Mltop.init_known_plugins (); diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index c41f16c95b..41bff34bd3 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -37,7 +37,7 @@ let vernac_echo ?loc in_chan = let open Loc in Feedback.msg_notice @@ str @@ really_input_string in_chan len ) loc -(* Reenable when we get back to feedback printing *) +(* Re-enable when we get back to feedback printing *) (* let is_end_of_input any = match any with *) (* Stm.End_of_input -> true *) (* | _ -> false *) diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index 445f10ecc1..9353ef3902 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -168,7 +168,7 @@ let rec traverse current ctx accu t = match Constr.kind t with let body () = id |> Global.lookup_named |> NamedDecl.get_value in traverse_object accu body (VarRef id) | Const (kn, _) -> - let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in + let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in traverse_object accu body (ConstRef kn) | Ind ((mind, _) as ind, _) -> traverse_inductive accu mind (IndRef ind) @@ -181,7 +181,7 @@ let rec traverse current ctx accu t = match Constr.kind t with | Lambda(_,_,oty), Const (kn, _) when Vars.noccurn 1 oty && not (Declareops.constant_has_body (lookup_constant kn)) -> - let body () = Option.map fst (Global.body_of_constant_body (lookup_constant kn)) in + let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in traverse_object ~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn) | _ -> diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 635751bb24..c37e90650a 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -146,7 +146,7 @@ let do_assumptions ~program_mode kind nl l = l [] else l in - (* We intepret all declarations in the same evar_map, i.e. as a telescope. *) + (* We interpret all declarations in the same evar_map, i.e. as a telescope. *) let (sigma,_,_),l = List.fold_left_map (fun (sigma,env,ienv) (is_coe,(idl,c)) -> let sigma,(t,imps) = interp_assumption ~program_mode sigma env ienv c in let r = Retyping.relevance_of_type env sigma t in diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 00f19f545c..a428c42e49 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -333,7 +333,7 @@ let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v | CStructRec na -> na | (CWfRec (na,_) | CMeasureRec (Some na,_,_)) when not structonly -> na | CMeasureRec (None,_,_) when not structonly -> - user_err Pp.(str "Decreasing argument must be specificed in measure clause.") + user_err Pp.(str "Decreasing argument must be specified in measure clause.") | _ -> user_err Pp.(str "Well-founded induction requires Program Fixpoint or Function.") diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index 568e5b9997..9bc225475d 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -546,6 +546,15 @@ let extend_constr state forpat ng = let constr_levels = GramState.field () +let is_disjunctive_pattern_rule ng = + String.is_sub "( _ | " (snd ng.notgram_notation) 0 + +let warn_disj_pattern_notation = + let open Pp in + let pp ng = str "Use of " ++ Notation.pr_notation ng.notgram_notation ++ + str " Notation is deprecated as it is inconsistent with pattern syntax." in + CWarnings.create ~name:"disj-pattern-notation" ~category:"notation" ~default:CWarnings.Disabled pp + let extend_constr_notation ng state = let levels = match GramState.get state constr_levels with | None -> String.Map.add "constr" default_constr_levels String.Map.empty @@ -553,8 +562,13 @@ let extend_constr_notation ng state = in (* Add the notation in constr *) let (r, levels) = extend_constr levels ForConstr ng in - (* Add the notation in cases_pattern *) - let (r', levels) = extend_constr levels ForPattern ng in + (* Add the notation in cases_pattern, unless it would disrupt *) + (* parsing nested disjunctive patterns. *) + let (r', levels) = + if is_disjunctive_pattern_rule ng then begin + warn_disj_pattern_notation ng; + ([], levels) + end else extend_constr levels ForPattern ng in let state = GramState.set state constr_levels levels in (r @ r', state) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index b2db64f74c..7c8c2b10ab 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -303,7 +303,7 @@ GRAMMAR EXTEND Gram [ [ "@{" ; l = LIST0 identref; ext = [ "+" -> { true } | -> { false } ]; cs = [ "|"; l' = LIST0 univ_constraint SEP ","; ext = [ "+" -> { true } | -> { false } ]; "}" -> { (l',ext) } - | ext = [ "}" -> { true } | "|}" -> { false } ] -> { ([], ext) } ] + | ext = [ "}" -> { true } | bar_cbrace -> { false } ] -> { ([], ext) } ] -> { let open UState in { univdecl_instance = l; diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 642695bda4..6ac259b1fe 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -219,7 +219,7 @@ let declare_one_case_analysis_scheme ind = let kelim = elim_sorts (mib,mip) in (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the - apropriate type *) + appropriate type *) if Sorts.List.mem InType kelim then ignore (define_individual_scheme dep UserAutomaticRequest None ind) diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 317cf487cc..740b9031cc 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -57,7 +57,7 @@ let retrieve_first_recthm uctx = function let uctx = UState.context uctx in let inst = Univ.UContext.instance uctx in let map (c, ctx) = Vars.subst_instance_constr inst c in - (Option.map map (Global.body_of_constant_body cb), is_opaque cb) + (Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb) | _ -> assert false let adjust_guardness_conditions const = function diff --git a/vernac/loadpath.ml b/vernac/loadpath.ml new file mode 100644 index 0000000000..f5e8b6d12f --- /dev/null +++ b/vernac/loadpath.ml @@ -0,0 +1,273 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +open Util +module DP = Names.DirPath + +(** Load paths. Mapping from physical to logical paths. *) + +type t = { + path_physical : CUnix.physical_path; + path_logical : DP.t; + path_implicit : bool; +} + +let load_paths = Summary.ref ([] : t list) ~name:"LOADPATHS" + +let logical p = p.path_logical +let physical p = p.path_physical + +let pp p = + let dir = DP.print p.path_logical in + let path = Pp.str (CUnix.escaped_string_of_physical_path p.path_physical) in + Pp.(hov 2 (dir ++ spc () ++ path)) + +let get_load_paths () = !load_paths + +let anomaly_too_many_paths path = + CErrors.anomaly Pp.(str "Several logical paths are associated to" ++ spc () ++ str path ++ str ".") + +let find_load_path phys_dir = + let phys_dir = CUnix.canonical_path_name phys_dir in + let filter p = String.equal p.path_physical phys_dir in + let paths = List.filter filter !load_paths in + match paths with + | [] -> raise Not_found + | [p] -> p + | _ -> anomaly_too_many_paths phys_dir + +let remove_load_path dir = + let filter p = not (String.equal p.path_physical dir) in + load_paths := List.filter filter !load_paths + +let warn_overriding_logical_loadpath = + CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" + (fun (phys_path, old_path, coq_path) -> + Pp.(seq [str phys_path; strbrk " was previously bound to " + ; DP.print old_path; strbrk "; it is remapped to " + ; DP.print coq_path])) + +let add_load_path phys_path coq_path ~implicit = + let phys_path = CUnix.canonical_path_name phys_path in + let filter p = String.equal p.path_physical phys_path in + let binding = { + path_logical = coq_path; + path_physical = phys_path; + path_implicit = implicit; + } in + match List.filter filter !load_paths with + | [] -> + load_paths := binding :: !load_paths + | [{ path_logical = old_path; path_implicit = old_implicit }] -> + let replace = + if DP.equal coq_path old_path then + implicit <> old_implicit + else + let () = + (* Do not warn when overriding the default "-I ." path *) + if not (DP.equal old_path Libnames.default_root_prefix) then + warn_overriding_logical_loadpath (phys_path, old_path, coq_path) + in + true in + if replace then + begin + remove_load_path phys_path; + load_paths := binding :: !load_paths; + end + | _ -> anomaly_too_many_paths phys_path + +let filter_path f = + let rec aux = function + | [] -> [] + | p :: l -> + if f p.path_logical then (p.path_physical, p.path_logical) :: aux l + else aux l + in + aux !load_paths + +let expand_path ?root dir = + let rec aux = function + | [] -> [] + | { path_physical = ph; path_logical = lg; path_implicit = implicit } :: l -> + let success = + match root with + | None -> + if implicit then Libnames.is_dirpath_suffix_of dir lg + else DP.equal dir lg + | Some root -> + Libnames.(is_dirpath_prefix_of root lg && + is_dirpath_suffix_of dir (drop_dirpath_prefix root lg)) in + if success then (ph, lg) :: aux l else aux l in + aux !load_paths + +let locate_file fname = + let paths = List.map physical !load_paths in + let _,longfname = + System.find_file_in_path ~warn:(not !Flags.quiet) paths fname in + longfname + +(************************************************************************) +(*s Locate absolute or partially qualified library names in the path *) + +type library_location = LibLoaded | LibInPath +type locate_error = LibUnmappedDir | LibNotFound +type 'a locate_result = ('a, locate_error) result + +let warn_several_object_files = + CWarnings.create ~name:"several-object-files" ~category:"require" + Pp.(fun (vi, vo) -> + seq [ str "Loading"; spc (); str vi + ; strbrk " instead of "; str vo + ; strbrk " because it is more recent" + ]) + + +let select_vo_file ~warn loadpath base = + let find ext = + let loadpath = List.map fst loadpath in + try + let name = Names.Id.to_string base ^ ext in + let lpath, file = + System.where_in_path ~warn loadpath name in + Some (lpath, file) + with Not_found -> None in + match find ".vo", find ".vio" with + | None, None -> + Error LibNotFound + | Some res, None | None, Some res -> + Ok res + | Some (_, vo), Some (_, vi as resvi) + when Unix.((stat vo).st_mtime < (stat vi).st_mtime) -> + warn_several_object_files (vi, vo); + Ok resvi + | Some resvo, Some _ -> + Ok resvo + +let locate_absolute_library dir : CUnix.physical_path locate_result = + (* Search in loadpath *) + let pref, base = Libnames.split_dirpath dir in + let loadpath = filter_path (fun dir -> DP.equal dir pref) in + match loadpath with + | [] -> Error LibUnmappedDir + | _ -> + match select_vo_file ~warn:false loadpath base with + | Ok (_, file) -> Ok file + | Error fail -> Error fail + +let locate_qualified_library ?root ?(warn = true) qid : + (library_location * DP.t * CUnix.physical_path) locate_result = + (* Search library in loadpath *) + let dir, base = Libnames.repr_qualid qid in + let loadpath = expand_path ?root dir in + match loadpath with + | [] -> Error LibUnmappedDir + | _ -> + match select_vo_file ~warn loadpath base with + | Ok (lpath, file) -> + let dir = Libnames.add_dirpath_suffix + (CString.List.assoc lpath loadpath) base in + (* Look if loaded *) + if Library.library_is_loaded dir + then Ok (LibLoaded, dir, Library.library_full_filename dir) + (* Otherwise, look for it in the file system *) + else Ok (LibInPath, dir, file) + | Error fail -> Error fail + +let error_unmapped_dir qid = + let prefix, _ = Libnames.repr_qualid qid in + CErrors.user_err ~hdr:"load_absolute_library_from" + Pp.(seq [ str "Cannot load "; Libnames.pr_qualid qid; str ":"; spc () + ; str "no physical path bound to"; spc () + ; DP.print prefix; fnl () + ]) + +let error_lib_not_found qid = + CErrors.user_err ~hdr:"load_absolute_library_from" + Pp.(seq [ str "Cannot find library "; Libnames.pr_qualid qid; str" in loadpath"]) + +let try_locate_absolute_library dir = + match locate_absolute_library dir with + | Ok res -> res + | Error LibUnmappedDir -> + error_unmapped_dir (Libnames.qualid_of_dirpath dir) + | Error LibNotFound -> + error_lib_not_found (Libnames.qualid_of_dirpath dir) + +(** { 5 Extending the load path } *) + +(* Adds a path to the Coq and ML paths *) +type add_ml = AddNoML | AddTopML | AddRecML + +type vo_path_spec = { + unix_path : string; (* Filesystem path containing vo/ml files *) + coq_path : DP.t; (* Coq prefix for the path *) + implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) + has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) +} + +type coq_path_spec = + | VoPath of vo_path_spec + | MlPath of string + +type coq_path = { + path_spec: coq_path_spec; + recursive: bool; +} + +let warn_cannot_open_path = + CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" + (fun unix_path -> Pp.(str "Cannot open " ++ str unix_path)) + +let warn_cannot_use_directory = + CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem" + (fun d -> + Pp.(str "Directory " ++ str d ++ + strbrk " cannot be used as a Coq identifier (skipped)")) + +let convert_string d = + try Names.Id.of_string d + with + | CErrors.UserError _ -> + let d = Unicode.escaped_if_non_utf8 d in + warn_cannot_use_directory d; + raise Exit + +let add_vo_path ~recursive lp = + let unix_path = lp.unix_path in + let implicit = lp.implicit in + if System.exists_dir unix_path then + let dirs = if recursive then System.all_subdirs ~unix_path else [] in + let prefix = DP.repr lp.coq_path in + let convert_dirs (lp, cp) = + try + let path = List.rev_map convert_string cp @ prefix in + Some (lp, DP.make path) + with Exit -> None + in + let dirs = List.map_filter convert_dirs dirs in + let add_ml_dir = Mltop.add_ml_dir ~recursive:false in + let () = match lp.has_ml with + | AddNoML -> () + | AddTopML -> + Mltop.add_ml_dir ~recursive:false unix_path + | AddRecML -> + List.iter (fun (lp,_) -> add_ml_dir lp) dirs; + add_ml_dir unix_path in + let add (path, dir) = add_load_path path ~implicit dir in + let () = List.iter add dirs in + add_load_path unix_path ~implicit lp.coq_path + else + warn_cannot_open_path unix_path + +let add_coq_path { recursive; path_spec } = match path_spec with + | VoPath lp -> + add_vo_path ~recursive lp + | MlPath dir -> + Mltop.add_ml_dir ~recursive dir diff --git a/library/loadpath.mli b/vernac/loadpath.mli index 4044ca1127..6605daa8d2 100644 --- a/library/loadpath.mli +++ b/vernac/loadpath.mli @@ -20,19 +20,15 @@ open Names type t (** Type of loadpath bindings. *) -val physical : t -> CUnix.physical_path -(** Get the physical path (filesystem location) of a loadpath. *) - val logical : t -> DirPath.t (** Get the logical path (Coq module hierarchy) of a loadpath. *) +val pp : t -> Pp.t +(** Print a load path *) + val get_load_paths : unit -> t list (** Get the current loadpath association. *) -val add_load_path : CUnix.physical_path -> DirPath.t -> implicit:bool -> unit -(** [add_load_path phys log type] adds the binding [phys := log] to the current - loadpaths. *) - val remove_load_path : CUnix.physical_path -> unit (** Remove the current logical path binding associated to a given physical path, if any. *) @@ -41,17 +37,53 @@ val find_load_path : CUnix.physical_path -> t (** Get the binding associated to a physical path. Raises [Not_found] if there is none. *) -val is_in_load_paths : CUnix.physical_path -> bool -(** Whether a physical path is currently bound. *) - -val expand_path : ?root:DirPath.t -> DirPath.t -> (CUnix.physical_path * DirPath.t) list -(** Given a relative logical path, associate the list of absolute physical and - logical paths which are possible matches of it. *) - -val filter_path : (DirPath.t -> bool) -> (CUnix.physical_path * DirPath.t) list -(** As {!expand_path} but uses a filter function instead, and ignores the - implicit status of loadpaths. *) - val locate_file : string -> string (** Locate a file among the registered paths. Do not use this function, as it does not respect the visibility of paths. *) + +(** {6 Locate a library in the load path } *) +type library_location = LibLoaded | LibInPath +type locate_error = LibUnmappedDir | LibNotFound +type 'a locate_result = ('a, locate_error) result + +val locate_qualified_library + : ?root:DirPath.t + -> ?warn:bool + -> Libnames.qualid + -> (library_location * DirPath.t * CUnix.physical_path) locate_result + +(** Locates a library by implicit name. + + @raise LibUnmappedDir if the library is not in the path + @raise LibNotFound if there is no corresponding file in the path + +*) + +val try_locate_absolute_library : DirPath.t -> string + +(** {6 Extending the Load Path } *) + +(** Adds a path to the Coq and ML paths *) +type add_ml = AddNoML | AddTopML | AddRecML + +type vo_path_spec = { + unix_path : string; + (** Filesystem path containing vo/ml files *) + coq_path : Names.DirPath.t; + (** Coq prefix for the path *) + implicit : bool; + (** [implicit = true] avoids having to qualify with [coq_path] *) + has_ml : add_ml; + (** If [has_ml] is true, the directory will also be search for plugins *) +} + +type coq_path_spec = + | VoPath of vo_path_spec + | MlPath of string + +type coq_path = { + path_spec: coq_path_spec; + recursive: bool; +} + +val add_coq_path : coq_path -> unit diff --git a/vernac/mltop.ml b/vernac/mltop.ml index 78e26c65d4..bbee9988d0 100644 --- a/vernac/mltop.ml +++ b/vernac/mltop.ml @@ -159,75 +159,9 @@ let add_ml_dir s = | _ -> () (* For Rec Add ML Path (-R) *) -let add_rec_ml_dir unix_path = - List.iter (fun (lp,_) -> add_ml_dir lp) (all_subdirs ~unix_path) - -(* Adding files to Coq and ML loadpath *) - -let warn_cannot_use_directory = - CWarnings.create ~name:"cannot-use-directory" ~category:"filesystem" - (fun d -> - str "Directory " ++ str d ++ - strbrk " cannot be used as a Coq identifier (skipped)") - -let convert_string d = - try Names.Id.of_string d - with UserError _ -> - let d = Unicode.escaped_if_non_utf8 d in - warn_cannot_use_directory d; - raise Exit - -let warn_cannot_open_path = - CWarnings.create ~name:"cannot-open-path" ~category:"filesystem" - (fun unix_path -> str "Cannot open " ++ str unix_path) - -type add_ml = AddNoML | AddTopML | AddRecML - -type vo_path_spec = { - unix_path : string; - coq_path : Names.DirPath.t; - implicit : bool; - has_ml : add_ml; -} - -type coq_path_spec = - | VoPath of vo_path_spec - | MlPath of string - -type coq_path = { - path_spec: coq_path_spec; - recursive: bool; -} - -let add_vo_path ~recursive lp = - let unix_path = lp.unix_path in - let implicit = lp.implicit in - if exists_dir unix_path then - let dirs = if recursive then all_subdirs ~unix_path else [] in - let prefix = Names.DirPath.repr lp.coq_path in - let convert_dirs (lp, cp) = - try - let path = List.rev_map convert_string cp @ prefix in - Some (lp, Names.DirPath.make path) - with Exit -> None - in - let dirs = List.map_filter convert_dirs dirs in - let () = match lp.has_ml with - | AddNoML -> () - | AddTopML -> add_ml_dir unix_path - | AddRecML -> List.iter (fun (lp,_) -> add_ml_dir lp) dirs; add_ml_dir unix_path in - let add (path, dir) = - Loadpath.add_load_path path ~implicit dir in - let () = List.iter add dirs in - Loadpath.add_load_path unix_path ~implicit lp.coq_path - else - warn_cannot_open_path unix_path - -let add_coq_path { recursive; path_spec } = match path_spec with - | VoPath lp -> - add_vo_path ~recursive lp - | MlPath dir -> - if recursive then add_rec_ml_dir dir else add_ml_dir dir +let add_ml_dir ~recursive unix_path = + let dirs = if recursive then (all_subdirs ~unix_path) else [unix_path,[]] in + List.iter (fun (lp,_) -> add_ml_dir lp) dirs (* convertit un nom quelconque en nom de fichier ou de module *) let mod_of_name name = diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 3d796aa4aa..b457c9c88f 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -32,6 +32,9 @@ val ocaml_toploop : unit -> unit (** {5 ML Dynlink} *) +(** Adds a dir to the plugin search path *) +val add_ml_dir : recursive:bool -> string -> unit + (** Tests if we can load ML files *) val has_dynlink : bool @@ -41,27 +44,6 @@ val dir_ml_load : string -> unit (** Dynamic interpretation of .ml *) val dir_ml_use : string -> unit -(** Adds a path to the Coq and ML paths *) -type add_ml = AddNoML | AddTopML | AddRecML - -type vo_path_spec = { - unix_path : string; (* Filesystem path contaning vo/ml files *) - coq_path : Names.DirPath.t; (* Coq prefix for the path *) - implicit : bool; (* [implicit = true] avoids having to qualify with [coq_path] *) - has_ml : add_ml; (* If [has_ml] is true, the directory will also be search for plugins *) -} - -type coq_path_spec = - | VoPath of vo_path_spec - | MlPath of string - -type coq_path = { - path_spec: coq_path_spec; - recursive: bool; -} - -val add_coq_path : coq_path -> unit - (** List of modules linked to the toplevel *) val add_known_module : string -> unit val module_is_known : string -> bool diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 46c4422d17..ad175511b9 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -331,7 +331,7 @@ let default_tactic = ref (Proofview.tclUNIT ()) let get_hide_obligations = Goptions.declare_bool_option_and_ref ~depr:false - ~name:"Hidding of Program obligations" + ~name:"Hiding of Program obligations" ~key:["Hide";"Obligations"] ~value:false diff --git a/vernac/search.ml b/vernac/search.ml index e41378908f..a5663d65ef 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -28,7 +28,7 @@ type display_function = GlobRef.t -> env -> constr -> unit [SearchAbout ...], etc. to the names of the symbols matching the query, separated by a newline. This type of output is useful for editors (like emacs), to generate a list of completion candidates -without having to parse thorugh the types of all symbols. *) +without having to parse through the types of all symbols. *) type glob_search_about_item = | GlobSearchSubPattern of constr_pattern diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 7f5c265eea..57c56a58f9 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -32,6 +32,7 @@ Assumptions Vernacstate Mltop Topfmt +Loadpath Vernacentries Misctypes diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 828356d31d..5ae572541e 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -201,11 +201,6 @@ let show_match id = (* "Print" commands *) -let print_path_entry p = - let dir = DirPath.print (Loadpath.logical p) in - let path = str (CUnix.escaped_string_of_physical_path (Loadpath.physical p)) in - Pp.hov 2 (dir ++ spc () ++ path) - let print_loadpath dir = let l = Loadpath.get_load_paths () in let l = match dir with @@ -215,7 +210,7 @@ let print_loadpath dir = List.filter filter l in str "Logical Path / Physical path:" ++ fnl () ++ - prlist_with_sep fnl print_path_entry l + prlist_with_sep fnl Loadpath.pp l let print_modules () = let opened = Library.opened_libraries () @@ -444,9 +439,9 @@ let locate_file f = str file let msg_found_library = function - | Library.LibLoaded, fulldir, file -> + | Loadpath.LibLoaded, fulldir, file -> hov 0 (DirPath.print fulldir ++ strbrk " has been loaded from file " ++ str file) - | Library.LibInPath, fulldir, file -> + | Loadpath.LibInPath, fulldir, file -> hov 0 (DirPath.print fulldir ++ strbrk " is bound to file " ++ str file) let err_unmapped_library ?from qid = @@ -471,10 +466,11 @@ let err_notfound_library ?from qid = (strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) let print_located_library qid = - try msg_found_library (Library.locate_qualified_library ~warn:false qid) - with - | Library.LibUnmappedDir -> err_unmapped_library qid - | Library.LibNotFound -> err_notfound_library qid + let open Loadpath in + match locate_qualified_library ~warn:false qid with + | Ok lib -> msg_found_library lib + | Error LibUnmappedDir -> err_unmapped_library qid + | Error LibNotFound -> err_notfound_library qid let smart_global r = let gr = Smartlocate.smart_global r in @@ -626,7 +622,7 @@ let vernac_end_proof ?pstate ?proof = function let vernac_exact_proof ~pstate c = (* spiwack: for simplicity I do not enforce that "Proof proof_term" is - called only at the begining of a proof. *) + called only at the beginning of a proof. *) let pstate, status = Pfedit.by (Tactics.exact_proof c) pstate in let pstate = save_proof_proved ?proof:None ~pstate ~opaque:Proof_global.Opaque ~idopt:None in if not status then Feedback.feedback Feedback.AddedAxiom; @@ -1026,18 +1022,18 @@ let vernac_require from import qidl = Some (Libnames.add_dirpath_suffix hd tl) in let locate qid = - try - let warn = not !Flags.quiet in - let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in - (dir, f) - with - | Library.LibUnmappedDir -> err_unmapped_library ?from:root qid - | Library.LibNotFound -> err_notfound_library ?from:root qid + let open Loadpath in + let warn = not !Flags.quiet in + match locate_qualified_library ?root ~warn qid with + | Ok (_,dir,f) -> dir, f + | Error LibUnmappedDir -> err_unmapped_library ?from:root qid + | Error LibNotFound -> err_notfound_library ?from:root qid in let modrefl = List.map locate qidl in if Dumpglob.dump () then List.iter2 (fun {CAst.loc} dp -> Dumpglob.dump_libref ?loc dp "lib") qidl (List.map fst modrefl); - Library.require_library_from_dirpath modrefl import + let lib_resolver = Loadpath.try_locate_absolute_library in + Library.require_library_from_dirpath ~lib_resolver modrefl import (* Coercions and canonical structures *) @@ -1133,7 +1129,7 @@ let expand filename = Envars.expand_path_macros ~warn:(fun x -> Feedback.msg_warning (str x)) filename let vernac_add_loadpath implicit pdir ldiropt = - let open Mltop in + let open Loadpath in let pdir = expand pdir in let alias = Option.default Libnames.default_root_prefix ldiropt in add_coq_path { recursive = true; @@ -1141,11 +1137,10 @@ let vernac_add_loadpath implicit pdir ldiropt = let vernac_remove_loadpath path = Loadpath.remove_load_path (expand path) - (* Coq syntax for ML or system commands *) let vernac_add_ml_path isrec path = - let open Mltop in + let open Loadpath in add_coq_path { recursive = isrec; path_spec = MlPath (expand path) } let vernac_declare_ml_module ~local l = diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 54e08d0e95..b37e527f47 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -22,7 +22,7 @@ a query like Check. The classification works on the assumption that we have 3 states: - parsing, execution (global enviroment, etc...), and proof + parsing, execution (global environment, etc...), and proof state. For example, commands that only alter the proof state are considered safe to delegate to a worker. |