| Age | Commit message (Collapse) | Author |
|---|
|
We make the primitives for backtrace-enriched exceptions canonical in
the `Exninfo` module, deprecating all other aliases.
At some point dependencies between `CErrors` and `Exninfo` were a bit
complex, after recent clean-ups the roles seem much clearer so we can
have a single place for `iraise` and `capture`.
|
|
- 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)
|
|
For instance, formerly, "Set Inline Level - 1" was succeeding. Now
only "Set Inline Level -1" succeeds. (Even though -1 does not make
sense for a Inline Level, but that's then a semantic issue. Other
options may accept negative numbers in general.)
|
|
|
|
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: herbelin
Reviewed-by: ppedrot
|
|
It is more convenient to use recent versions of OCaml while developing
(better backtraces, etc).
|
|
building votour
Reviewed-by: ppedrot
|
|
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
|
|
Reviewed-by: Zimmi48
|
|
Ack-by: ejgallego
|
|
|
|
|
|
They were in Ltac2, but they are of general interest
|
|
|
|
|
|
|
|
Fixes #11726
|
|
|
|
In case no eliminator is given, we wait until `get_eliminator` to
produce the actual eliminator. Using the sigma produced by guess_elim
here would insert an unused universe for the predicate's type in the
sigma.
|
|
We provide the closure of the dependencies manually.
This is still a hack, but not so bad given that the `source`'d files
still do contain that duplication too.
Dune should provide this functionality so we can replace both this
rule and the source files. Actually, that's not hard to implement,
`utop` already supports a printer attribute so these are loaded
automatically, so the ocamldebug mode could do the same.
Should fix #11716
|
|
Reviewed-by: cpitclaudel
|
|
The previous code was only doing that when either in debug or toplevel mode.
Unfortunately, when dealing with open modules the constants might not have
been registered yet, leading to printing failure. I do not see a reason
why this code should fail when used with globals without a user facing name
when the only goal is to compute a set of identifiers that might clash. Thus,
the above failsafe behaviour is now systematic.
Fixes #8206: Module signature error sometimes prints ??.
|
|
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
|
|
This is in preparation for making the Gramlib interface the canonical
one; see #11647 .
I tried to implement some of the ideas that were floated around in a
chat with Pierre-Marie, suggestions / comments are welcome.
|
|
Ack-by: SkySkimmer
Ack-by: Zimmi48
|
|
|
|
It was not documented, I do not think it is used in the wild, and it relies
on legacy code. As solid conjunction of reasons that support its deprecation.
|
|
|
|
Fixes #11608.
This means -vos doesn't skip proofs for definitions that end with Qed
but don't include Proof and rely on a Set Default Proof Using. However,
this fixes the bug where this pattern would instead hang, due to #11564.
|
|
|
|
|
|
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.
|
|
|
|
See "https://github.com/coq/coq/pull/10008#discussion_r382899607".
|
|
Compile buffer, and with building from a path containing spaces.
Updated CHANGES.md
Now using Filename.quote instead of enclosing in single quotes.
Fixed rebasing problems.
|
|
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
`Nativelib` currently assumes that objects are built in some
particular directories, but this is not true in some cases, for
example, when building with Dune.
We add a new option `-nI` to allow clients to specify the OCaml
include dirs.
|
|
This is useful in order to implement native support in Dune for
example, which as of today as strict target rules.
Hopefully this option could go away; it is really internal, but I've
chosen to document it.
|
|
Reviewed-by: herbelin
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
Reviewed-by: thery
|
|
We avoid redundant notations for the same concepts and make sure
notations do not break Ltac parsing for users of these libraries.
|
