| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: gares
|
|
Most functions are taken either from the Coq standard library or the
OCaml standard library. One (`enumerate`) is taken from Python. Most
names are chosen according to OCaml conventions (as Coq does not have
exceptions, and so the OCaml naming conventions already distinguish
between option and exception). Since `exists` is a keyword, we use the
Coq name `existsb` instead. We generally favor Coq argument ordering
when there is a conflict between Coq and OCaml.
Note that `seq` matches neither Coq nor OCaml; it takes a `step`
argument for how much to increment by on each step.
Sorting functions are mostly taken from Coq's mergesort library; it
might make sense to replace them with OCaml's versions for efficiency?
|
|
|
|
|
|
|
|
|
|
|
|
- use coqc instead of coqtop (since -compile doesn't work anymore this
is better)
- pass through extra arguments to dune-dbg
- auto detect the need to pass -emacs to ocamldebug
- instructions for emacs users
The dune-dbg dependencies are still broken ;_;
|
|
|
|
Co-Authored-By: @Zimmi48
|
|
|
|
|
|
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
generalization + cleanups
Reviewed-by: herbelin
|
|
Reviewed-by: Zimmi48
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: cpitclaudel
Reviewed-by: gares
Reviewed-by: jfehrle
Reviewed-by: vbgl
|
|
Reviewed-by: Zimmi48
|
|
|
|
|
|
|
|
Reviewed-by: vbgl
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Typeclasses resolution is not used anymore for lia.
Typeclasses resolution is still used by lra but only to access a
database of declared constants.
|
|
|
|
|
|
Closes #8735 .
|
|
The recursive functions and their binders were not pushed in the right
order for implicit arguments.
Additionally, we avoid calling push_name_env both for interpreting the
type of each component of a (co-)fixpoint and for interpreting again the
body of each component of a (co-)fixpoint because it may have
side-effects (in the glob file). So we instead remember the part of
its action on implicit arguments to replay it functionally.
|
|
|
|
|
|
This seems more robust and avoids having another implementation of
`cp`.
|
|
|
|
We cleanup a bit the implementation of LoadPath which is not possible
as now all the loadpath logic is in the same place.
In particular, we remove exceptions in favor a `locate_result` monad.
More cleanup should still be possible, in particular
`locate_absolute_library` and `locate_qualified_library` should be
merged.
|
|
We consolidate loadpath handling as a single `Loadpath` module from
parts in `Library` and `Mltop`, placing it at the `vernac` level [as
`Mltop`]
This idea was first suggested in https://github.com/coq/coq/pull/9808
, and indeed it makes sense as library resolution tends to be business
of the upper layers: IDE / build tools.
Logic could be pushed upwards, but this is good enough for now.
This consolidation has enabled some good and long overdue
refactorings, and the module should become self-contained enough as to
allow the resolution logic to be shared with `coqdep` in the future.
The `Mltop` module only cares now about ML-level modules, and should
go away once we rewrite the loader using `findlib` to solve
https://github.com/coq/coq/issues/7698 .
|
|
Reviewed-by: gares
|
|
Ack-by: gares
Ack-by: herbelin
Reviewed-by: vbgl
|
|
|
|
This lets us avoid passing ~ontop to do_definition and co, and after #10050
to even more functions.
|
|
|
|
It's used a few times in the stdlib (a couple of which need no other
change when removing the !) and not at all throughout our CI.
Considering that I think it's fair enough to remove it.
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Reviewed-by: gares
Reviewed-by: maximedenes
|
|
Ack-by: herbelin
Reviewed-by: maximedenes
Ack-by: ppedrot
|
|
|
|
This code was originally part of #8811, authored by Gaëtan Gilbert.
It seems we are not very consistent on what we do when we use
`ParameterEntry`, specially w.r.t. universes but as code cleanup
progresses we will have a better view.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
By construction, we know that Cooking is returning the right set of
used variables. This set has been checked already once at the time
when the definition was performed inside the section.
|
|
This removes a lot of cruft breaking the opaque proof abstraction in
Safe_typing and similar.
|
|
Reviewed-by: JasonGross
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
|
