| Age | Commit message (Collapse) | Author |
|---|
|
We try to encapsulate the future goals abstraction in the evar map.
A few calls to `save_future_goals` and `restore_future_goals` are still
there, but we try to minimize them.
This is a preliminary refactoring to make the invariants between the
shelf and future goals more explicit, before giving unification access
to the shelf, which is needed for #7825.
|
|
factorization in recursive notations
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
Reviewed-by: ppedrot
|
|
+ help on using option -f
Reviewed-by: jfehrle
Ack-by: herbelin
|
|
Ack-by: Zimmi48
Reviewed-by: jfehrle
Reviewed-by: ppedrot
Reviewed-by: thery
|
|
|
|
Add a mli file and uniformize indentation on the way.
|
|
The fix is a missing check of equality of custom entries. The enhancements are:
- not to bother breaking hints
- not to care about the border or internal position when the level is
made explicit
Ideally, one could also improve the treatment of DefaultLevel. To be
done later on.
|
|
This focuses review requests to bench-maintainers instead of sharing
with ci-maintainers
|
|
The purpose of `NsatzTactic` is to allow using `nsatz` without the
dependency on real axioms. So we declare the instances for `Z` and `Q`
in that file, so that users don't have to re-create them.
Fixes #12860
|
|
On GitLab, we don't need to base the job info on the PR number, since
it ought to be available from the git repo. Removing the logic will
make the bench infrastructure more uniform.
|
|
Reviewed-by: ejgallego
Ack-by: Alizter
Ack-by: gares
|
|
Reviewed-by: Zimmi48
|
|
This is a footgun as it can refresh the name. Callers can still ignore
the generated name by doing `intro_using_then id (fun _ -> tclUNIT())`.
|
|
This makes the test suite Omega.v compatible with Mangle Names
Not sure how `reintroduce` works since it ignores the refreshed name,
considering omega is deprecated it's not worth figuring out so long as
it works (NB making it use intro_mustbe_force makes the test suite
fail so it must be doing something right).
|
|
|
|
|
|
Fix #12676
|
|
Reviewed-by: SkySkimmer
|
|
Ack-by: Zimmi48
Reviewed-by: anton-trunov
|
|
|
|
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: ejgallego
|
|
|
|
Reviewed-by: SkySkimmer
Ack-by: ppedrot
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
|
|
Fix #12688.
Original test:
~~~coq
Record my_mod: Type := mk { datatype: Type; }.
Print Universes Subgraph (my_mod.u0). (* OK *)
From ITree Require Export ITree. (* using coq-itree for the sake of example *)
Print Universes Subgraph (my_mod.u0). (* Runs forever (> 1 min) *)
~~~
The issue is that we produce a subgraph with the user-given universes
+ Set and Prop. In the test the user given universes are not connected
to other universes, but Set is below every universe so we traverse the
whole graph.
We can go faster by just checking whether Set is strictly below each
universe we're interested in.
Maybe this would be better handled at the ugraph level but that
requires thinking about lbound so I didn't do it.
I tested locally with Require Reals, which makes the print take about
0.1s on my PC before this patch. This is enough to check that we're
now faster (near-instant) but not enough for automatic testing.
Note that the other uses of UGraph.constraints_for (for private
polymorphic universes and for context restriction) are interested in
all ambient universes so the traversals starting at Set end quickly
and do not cause the same issue.
|
|
Reviewed-by: SkySkimmer
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Tests moved in https://github.com/whonore/Coqtail/pull/134.
|
|
Added user overlay for bignums
|
|
Reviewed-by: anton-trunov
|
|
documentation
Reviewed-by: SkySkimmer
Reviewed-by: herbelin
Reviewed-by: jfehrle
|
|
recognition.
Reviewed-by: mattam82
|
|
|
|
|
|
Reviewed-by: mattam82
Ack-by: ppedrot
|
|
|
|
Reviewed-by: SkySkimmer
|
|
exist
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
of artificial dependencies disappearing by reduction
Reviewed-by: ppedrot
|
|
Now that 4.11.0 is released the trunk job doesn't work.
4.12 also doesn't work for separate reasons ("No rule found for
kernel/byterun/byterun.a")
We will separately update the edge switch in the docker image to use 4.11.0.
|
|
|
