| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ppedrot
|
|
We follow the solution used upstream
https://github.com/ocaml/ocaml/pull/2279
Fixes half of #10602
|
|
Reviewed-by: Zimmi48
|
|
This governs the printing of the explicitation of implicit arguments
and the removal of coercions.
E.g., "Check coe foo." where coe is a coercion with codomain B will show:
foo
: B
instead of
coe foo
: B
|
|
This approach using `type t = { sec_prev: t option; sec_... }` makes
it easy to update sections using the record update syntax, but
impossible to statically ensure that an operation only affects the
current section.
We may instead consider using `type t = section * section list` which
needs some boilerplate to update.
|
|
`dev/header.c` is not registered as a dependency, so the configure
step under dune fails in 32bit builds.
Note we don't detect the problem due to dubious code in configure
ignoring stderr messages on process calls.
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
|
|
Fixes #10971
|
|
|
|
|
|
This allows to give access to all printing options (e.g. a scope or
being-in-context) to every printer w/o increasing the numbers of
functions.
|
|
Ack-by: Zimmi48
Ack-by: herbelin
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
It seems this passed under my radar, but the change of implementation of the
safe demarshaller introduced by native integers and floating point numbers is
dangerous.
For floats, it makes the demarshaller depend on float kernel representation.
This is just an alias to the standard OCaml float type, so this is currently
not problematic, but this makes the code fragile if ever we decide to change
it there. This would trigger unsound object casts without any complaint from
the type-checker. Furthermore, having such a low-level library depend on
the kernel library sounds like a anti-feature to me.
For native integers, the situation is direr. The demarshaller turns
unconditionally 64-bits integers into their Int63 representation, which
depends on the architecture. This means that when parsing vo files from
a architecture where these types are not the same, we are guaranteed to get
into unsound casts. Some of them *might* get caught by the value
representation checker, yet it is a footgun. The demarshaller should only
deal with OCaml representations and not try to mess with Coq specific
data types, otherwise we are going to face desynchronization and thus
unsound casts.
|
|
Ack-by: Zimmi48
|
|
Reviewed-by: Zimmi48
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
|
|
Ack-by: Zimmi48
Reviewed-by: ejgallego
|
|
Failing on CProdN([],...) was maybe a bit too radical.
|
|
|
|
Reviewed-by: ppedrot
|
|
- Warn in some places where {x:T} is not assumed to occur (e.g. in
argument of an application, or of a match).
- Warn when an implicit argument occurs several times with the same name.
- Accept local anonymous {_:T} with explicitation possible using name `arg_k`.
We obtain this by using a flag (impl_binder_index) which tells if we
are in a position where implicit arguments matter and, if yes, the
index of the next binder.
|
|
This moves the encoding of "n" as "arg_n" closer to the user interface level.
Note however that Constrintern.build_impl is not able yet to use ExplByPos.
See further commits.
|
|
doc/changelog/02-specification-language/11233-master+fix11231-missing-variable-pattern-matching-decompilation.rst
OK, thanks.
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
|
|
This is the minimal set of changes requires for Coq to build under 2.0
mode. We may likely take advantage of some more new features.
Note that Dune 2.0 requires OCaml >= 4.06.0, OPAM allows to use Dune
in older versions as it will install a secondary compiler.
|
|
doc/changelog/03-notations/11172-master+coercion-notation-interleaved-printing.rst
Co-Authored-By: Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>
|
|
We renounce to the ad hoc rule preferring a notation w/o delimiter
for a term with coercions stripped over a notation for the
fully-applied terms with coercions not removed.
Instead, we interleave removal of coercions and search for notations:
we prefer a notation for the fully applied term, and, if not, try to
remove one coercion, and try again a notation for the remaining term,
and if not, try to remove the next coercion, etc.
Note: the flatten_application could be removed if prim_token were able
to apply on a prefix of an application node.
|
|
Reviewed-by: JasonGross
Reviewed-by: ejgallego
Reviewed-by: maximedenes
|
|
This is incorrect and has created some problems. We also remove
unneeded `dynlink` dep.
Closes #11217
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: maximedenes
|
|
Reviewed-by: gares
|
|
The missing dependency impacted the algorithm for detecting default
clauses.
|
