| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
|
|
Ack-by: SkySkimmer
Reviewed-by: jfehrle
Reviewed-by: ppedrot
|
|
Reviewed-by: Matafou
|
|
Reviewed-by: vbgl
|
|
Most of the parameters were named, we fix the remaining cases.
|
|
- Legacy attributes can now be specified in any order.
- Legacy attribute Cumulative maps to universes(cumulative).
- Legacy attribute NonCumulative maps to universes(noncumulative).
- Legacy attribute Private maps to private(matching).
We use "private(matching)" and not "private(match)" because we cannot
use keywords within attributes.
|
|
Reviewed-by: JasonGross
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
This enforces monomorphism everywhere possible.
|
|
Reviewed-by: ejgallego
Reviewed-by: ppedrot
|
|
|
|
Reviewed-by: jfehrle
|
|
Add headers to a few files which were missing them.
|
|
We reuse the same type as for options, even though it is a bit ill-named. At
least it allows to share code with it.
|
|
The current implementation was seemingly never thought for this kind of
semantics. Everything is superglobal by construction, notably hint database
creation and naming schemes. The new mode feels a bit hackish to me, at
some point this should be fully reimplemented from scratch with a clear
design in mind.
|
|
Fixes #11846: Funind fails to generate principles for terms with let bindings.
|
|
Since tclOR/tclORELSE are not supposed to return critical exceptions,
we don't need to replace catchable_exception by noncritical.
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: fajb
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
|
|
|
|
This is only used in `Ccalgo` and it does not provide any advantage
these days over the upstream OCaml implementation.
|
|
Reviewed-by: ppedrot
|
|
|
|
following the model of `pose (x:=t)`.
Reviewed-by: Zimmi48
Reviewed-by: ppedrot
|
|
Only significant change is in gcd / lcm which now are typed in `Z.t`
|
|
Reviewed-by: vbgl
|
|
Reviewed-by: Matafou
Reviewed-by: ppedrot
|
|
Reviewed-by: Zimmi48
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
This fixes #11547 ; note that it is hard to register such handlers in
the `Summary` due to layering issues; there are potential anomalies here
depending on how plugins do register their data structures.
|
|
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)
|
|
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".
|
|
|
|
|
|
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.
|
|
argument
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
This was redundant with `iraise`; exceptions in the logic monad now
are forced to attach `info` to `Proofview.NonLogical.raise`
|
|
"refresh" argument
Reviewed-by: ppedrot
|
|
Also renamed it to relative_entry_level.
Correspondence between old and new representation is:
(n,L) -> LevelLt n
(n,E), (n,Prec n) -> LevelLe n
(n,Any) -> LevelSome
(n,Prec p) when n<>p was unused
Should not change global semantics (except error message in pr_arg).
|
|
This PR is in preparation of #9067 (together with #11647) .
Before this PR, `grammar_extend` always took an optional `reinit`
argument, even if it was never set to `Some ...`. Indeed, there is a
single case where reinit is needed; we track it now by using a
different extension rule constructor.
|
|
It's been ignored since the introduction of universe polymorphism.
|
|
notation format + new notion of format associated to a given interpretation
Ack-by: maximedenes
|
|
This was due to an inconsistency in handling implicit arguments in
the fields and in the constructor of a record.
|
|
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
Reviewed-by: ppedrot
|
