| Age | Commit message (Collapse) | Author |
|---|
|
|
|
Same as #11780 except that this part can be backported to v8.11.
|
|
|
|
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
following the model of `pose (x:=t)`.
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
"where"-based notation
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: vbgl
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
|
|
This PR refactors the handling of ML loadpaths to get it closer to
what (as of 2020) the standard OCaml toolchain (ocamlfind, dune) does.
This is motivated as I am leaning toward letting the standard OCaml
machinery handle OCaml includes; this has several benefits [for
example plugins become regular OCaml libs] It will also help in
improving dependency handling in plugin dynload.
The main change is that "recursive" ML loadpaths are no longer
supported, so Coq's `-I` option becomes closer to OCaml's semantics.
We still allow `-Q` to extend the OCaml path recursively, but this may
become deprecated in the future if we decide to install the ML parts
of plugins in the standard OCaml location.
Due to this `Loadpath` still hooks into `Mltop`, but other than that
`.v` location handling is actually very close to become fully
independent of Coq [thus it can be used in other tools such coqdep,
the build system, etc...]
In terms of vernaculars the changes are:
- The `Add Rec ML Path` command has been removed,
- The `Add Loadpath "foo".` has been removed. We now require that the
form with the explicit prefix `Add Loadpath "foo" as Prefix.` is used.
We did modify `fake_ide` as not to add a directory with the empty
`Prefix`, which was not used. This exposed some bugs in the
implementation of the document model, which relied on having an
initial sentence; we have workarounded them just by adding a dummy one
in the two relevant cases.
|
|
- zify_iter_specs is entirely in OCaml
- zify_op has been improved
* The generation of proof-terms is more direct
* It does not `rewrite` but instead either performs
a `pose proof` or a `change`
* The support for `and`, `or`, `not`, arrow is hardcoded
* Avoid generating duplicate hypotheses such as 0 <= Z.of_nat x
- zify_elim_let is entirely in OCaml (no Ltac callback)
[micromega] fix stack overflow
Less naive computation of bounds (online elimination of duplicates)
|
|
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmi@gmail.com>
|
|
This is to be consistent with "pose (x:=a)" (and an alternative to
"assert (x:=a)").
This was suggested by
"https://github.com/HoTT/HoTT/pull/1208#discussion_r374342962".
|
|
Reviewed-by: cpitclaudel
|
|
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
|
|
|
|
Interestingly, the documentation for Hint Resolve -> qualid was outdated.
It was claiming that any term would be accepted, but actually with this
particular syntax, only qualified names would be parsed already.
|
|
We restrict hints to be global references, so as to further simplify the
implementation. Allowing arbitrary terms makes it difficult or expensive
to handle properly some actions like universe contexts or hint equality.
Ultimately, the IsConstr constructor for hints should also be removed.
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
|
|
We avoid redundant notations for the same concepts and make sure
notations do not break Ltac parsing for users of these libraries.
|
|
Reviewed-by: ejgallego
|
|
Show effect of edits to edited nt in PRINT
Add cmdv:: info to prodnCommands
Supporting code globally replaces a given "substring" in productions
with another. (Substring over doc_symbols, not over characters.)
|
|
those in the rsts.
|
|
|
|
|
|
|
|
|
|
(inconsistencies in parsing/printing notations to partial applications)
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: jfehrle
|
|
Reviewed-by: jfehrle
|
|
They were already deprecated in two major releases.
|
|
|
|
|
|
doc/changelog/03-notations/11120-master+refactoring-application-printing.rst
Thanks
Co-Authored-By: Jim Fehrle <jim.fehrle@gmail.com>
|
|
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
|
|
reserve parsing keywords
Reviewed-by: ejgallego
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: Zimmi48
Reviewed-by: herbelin
|
|
notation format + new notion of format associated to a given interpretation
Ack-by: maximedenes
|
|
This is useful when we want to have finer control of the location of
files in the bootstrap process, for example when building using Dune.
Also, this makes options consistent with what `coqdep` already uses
for bootstrap.
The main use case for `-boot` is to replace the hardcoded `add_load_path (coqlib () / theories)` with `-R dir Coq`, where dir is controlled by the build system. In particular, we use `-R . Coq` as we `cd` into the directory the package is, so without boot we'd have to hardcode the `theories` path in Dune itself. which seems less robust.
Notably after this change the only part of the build that uses `coqlib` is the micromega solver, but that can be tweaked so if coqlib is not set it will use the one in the path. IMO not having to set "coqlib" is a good property if we want a more compositional setup.
|
