| Age | Commit message (Collapse) | Author |
|---|
|
I think the usage looks cleaner this way.
|
|
Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: ejgallego
Ack-by: gares
Ack-by: maximedenes
Ack-by: ppedrot
|
|
Ack-by: herbelin
Reviewed-by: ppedrot
|
|
This work makes it possible to take advantage of a compact
representation for integers in the entire system, as opposed to only
in some reduction machines. It is useful for heavily computational
applications, where even constructing terms is not possible without such
a representation.
Concretely, it replaces part of the retroknowledge machinery with
a primitive construction for integers in terms, and introduces a kind of
FFI which maps constants to operators (on integers). Properties of these
operators are expressed as explicit axioms, whereas they were hidden in
the retroknowledge-based approach.
This has been presented at the Coq workshop and some Coq Working Groups,
and has been used by various groups for STM trace checking,
computational analysis, etc.
Contributions by Guillaume Bertholon and Pierre Roux <Pierre.Roux@onera.fr>
Co-authored-by: Benjamin Grégoire <Benjamin.Gregoire@inria.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>
|
|
[About] still says it.
Close #9056.
|
|
Since it returns an Id.t and not a Pp.t.
|
|
|
|
|
|
Diff code uses the lexer to recognize tokens in the inputs, which can be
Pp.t's or strings. To add the highlights in the Pp.t, the diff code
matches characters in the input to characters in the tokens. Current
code fails for inputs containing quote marks or "(*" because the quote
marks and comments don't appear in the tokens. This commit adds a "diff
mode" to the lexer to return those characters, making the diff routine
more robust.
|
|
|
|
You can tell which it is from the `@{}` if you really care, and seeing
`Monomorphic List (A:Type)` with no indication that `Monomorphic` is
about universes can confuse people.
|
|
- deprecate the old 5-tuple accessor in favor of a view record,
- move `name` and `kind` proof data from `Proof_global` to `Proof`,
this will prove useful in subsequent functionalizations of the
interface, in particular this is what abstract, which lives in the
monads, needs in order no to access global state.
- Note that `Proof.t` and `Proof_global.t` are redundant anyways.
|
|
|
|
These modules do actually belong there.
We have to slightly reorganize printers, removing a couple of
duplicated ones in the way.
|
|
|
|
|
|
|
|
Improve debug output
|
|
This is a pre-requisite to use automated formatting tools such as
`ocamlformat`, also, there were quite a few places where the comments
had basically no effect, thus it was confusing for the developer.
p.s: Reading some comments was a lot of fun :)
|
|
write_function
|
|
Set Printing Universes.
Set Universe Polymorphism.
Lemma foo : Type.
Proof. exact (forall _ : Type, Type).
Qed.
Print foo.
Before:
(*
foo@{Top.1} =
Type@{Top.2} -> Type@{Top.3}
: Type@{Top.1}
(* Top.1 |= Prop < Set
Set < Top.1
local: {Top.3 Top.2} |= Top.2 < Top.1
Top.3 < Top.1
*)
foo is universe polymorphic
*)
Now:
(* Public universes:
Top.1 |= Set < Top.1
Private universes:
{Top.3 Top.2} |= Top.2 < Top.1
Top.3 < Top.1 *)
|
|
|
|
|
|
|
|
|
|
We remove the `Proof_types` file which was a trivial stub, we also
cleanup a few layers of aliases.
This is not a lot but every little step helps.
|
|
This makes the make-based build system stop linking to Camlp5's
gramlib and instead links to our own gramlib.
We use the style done in the packing of `Stdlib` in OCaml 4.07.
As to introduce a minimal amount of noise in history we use an
autogenerated `gramlib__pack` directory.
Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>
|
|
|
|
|
|
This is documented in dev/doc/changes.md.
|
|
|
|
|
|
Close #8891
|
|
Allow for new goals that don't map to old goals
Include background_goals in all_goals return value
Fix incorrect change to raw diffs in shorten_diff_span
Fixes #8922
|
|
|
|
|
|
We move `object_prefix` to `Nametab`. This highlights the coupling of
`Lib` and `Nametab` wrt naming.
This also thins `Libname`, which IMHO is a good thing as we are
talking about "local, internal" naming here.
|
|
This type is "private" to the Nametab, which manages it. It thus makes
sense IMHO to live there.
|
|
|
|
This introduces a bit of noise in the Dune files but for now I think
it is the best way to do it.
|
|
`object_name` is a particular choice of the implementation of
`Liboject`, thus it makes sense to tie it to that particular module.
This may prove useful in the future as we may want to modify object
naming.
|
|
|
|
Removing a few Global.env in the way.
|
|
In general, `Nametab` is not a module you want to open globally as it
exposes very generic identifiers such as `push` or `global`.
Thus, we remove all global opens and qualify `Nametab` access. The
patch is small and confirms the hypothesis that `Nametab` access
happens in few places thus it doesn't need a global open.
It is also very convenient to be able to use `grep` to see accesses to
the namespace table.
|
|
interning/printing
|
|
|
|
This refines the fix to #2169 by distinguishing the short and
non-short printing modes.
This prepares functionalization of printers by always passing env
rather than setting env to None in short mode. This is not strictly
necessary for the env which is not used for printing global references
but it shall be more consistent in style when passing e.g. the nametab
functionally.
We however keep the fallback printer used in case of error while
printing: due to missing registration of submodule fields in the
nametab, printing with types does not work if there are references to
an inner module.
|
|
A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
|
|
We remove sections paths from kernel names. This is a cleanup as most of the times this information was unused. This implies a change in the Kernel API and small user visible changes with regards to tactic qualification. In particular, the removal of "global discharge" implies a large cleanup of code.
Additionally, the change implies that some machinery in `library` and `safe_typing` must now take an `~in_section` parameter, as to provide the information whether a section is open or not.
|
|
Fixes #6764: Printing Notation regressed compared to 8.7
|
