| Age | Commit message (Collapse) | Author |
|---|
|
Fix #12930
|
|
We remove some dead aliases and add some documentation to the
interface file.
|
|
Reviewed-by: gares
Reviewed-by: ppedrot
Reviewed-by: silene
|
|
|
|
|
|
|
|
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.
|
|
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.
|
|
|
|
Ack-by: SkySkimmer
Reviewed-by: herbelin
|
|
Reviewed-by: SkySkimmer
Ack-by: gares
|
|
|
|
Reviewed-by: herbelin
Reviewed-by: maximedenes
|
|
|
|
Try just going with the user-given names, and not worrying about
what happens with repeated names or anonymous implicits.
(Support for anonymous implicits is due to herbelin in #11098.)
This PR should not change behaviour in the absence of repeated names.
Since repeated names are already a poorly handled corner case, I would
recommend changing binder names to avoid overlap in the case of a
change in behavior.
Since anonymous implicits and implicits with repeated names can already
happen, I think this is unlikely to cause too many new problems,
though it might exacerbate existing ones. However, I already had to fix
one newly possible anomaly, so I can't be too confident.
The most common change in external developments was that an argument
no longer gets `0` appended to it, causing the `Arguments` command
to complain about renaming.
To fix this and keep the old name, one can simply use the `rename` flag
as suggested, or switch to the new, un-suffixed name.
Closes #6785
Closes #12001
Another step towards checking the standard library with `-mangle-names`.
|
|
|
|
Reviewed-by: ppedrot
|
|
Defined constants
Reviewed-by: ppedrot
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego
|
|
Helps with #12566
|
|
|
|
declaration path
Reviewed-by: ppedrot
|
|
Reviewed-by: SkySkimmer
|
|
|
|
generic printing format in anticipation of further not-only-parsing uses of the notation
Reviewed-by: ppedrot
|
|
This is a leftover after the unification of constant information,
`kind` is now correctly set by the single caller of
`Obls.add_mutual_definitions`.
|
|
Ack-by: gares
Reviewed-by: ppedrot
|
|
This is about the third time I try to kill this file but for some reason
it is still here.
|
|
Fixes #11970.
|
|
This is to anticipate further not-only-parsing uses of the notation.
|
|
This is an alternative to #12663 ; much preferable as the kind
information is already stored in the constant object.
|
|
Exceptions should not printed except for the top-level.
There is the weird anomaly-absorbing code in `Reductionops`, I wonder
how frequent that case is, but as the exception is absorbed printing
there could have a real impact.
|
|
This requires updating the parameter count at section end, I felt it
was easier to do with rebuild_function but it could be done in
discharge if needed.
Incidentally fixes #12649.
|
|
|
|
This is also needed in equations.
|
|
|
|
This is for use in Equations. At some point we should make all hook aware
of state, but this should suffice for now.
Note the comments as the role of hooks here, this may need further
cleanup indeed.
|
|
This is already taken of by `declare_definition`, by consistency with
the mutual case.
|
|
In our quest to unify all the declaration paths, an important step
is to account for the state pertaining to `Program` declarations.
Whereas regular proofs keep are kept in a stack-like structure;
obligations for constants defined by `Program` are stored in a global
map which is manipulated by almost regular open/close proof primitives.
We make this manipulation explicit by handling the program state
functionally, in a similar way than we already do for lemmas.
This requires to extend the proof DSL a bit; but IMO changes are
acceptable given the gain.
Most of the PR is routine; only remarkable change is that the hook is
called explicitly in `finish_admitted` as it had to learn about the
different types of proof_endings.
Note that we could have gone deeper and use the type system to refine
the core proof type; IMO it is still too preliminary so it is better
to do this step as an intermediate one towards a deeper unification.
|
|
This is essential to allow hooks to modify state.
|
|
Reviewed-by: ejgallego
|
|
Reviewed-by: ejgallego
Reviewed-by: herbelin
|
|
Reviewed-by: ejgallego
|
|
It used to be a big functor but changed in
8c5adfd5acb883a3bc2850b6fc8c29d352a421f8
The functor indent is now incorrect.
|
|
Fix #12651
|
|
Persistent arrays expose a functional interface but are implemented
using an imperative data structure. The OCaml implementation is based on
Jean-Christophe Filliâtre's.
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes
|
|
Fix #12551
|
