| Age | Commit message (Collapse) | Author |
|---|
|
Reviewed-by: ejgallego
Reviewed-by: jashug
|
|
This fixes #9767 by silently ignoring input lines which are not valid
UTF-8. We hereby assume that all file paths are valid UTF-8.
We also now actually test both python2 and python3 on the CI.
|
|
See https://gitlab.com/coq/coq/-/jobs/187496964
|
|
(warn if bar is a nonprimitive projection)
|
|
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: gares
Ack-by: pi8027
|
|
Reviewed-by: Zimmi48
|
|
- test-suite/bugs/closed/xx.v renamed to .../bug_xx.v
- test-suite/failure/inductive4.v is now .../inductive.v
- repro for #4157 now added to the repo (it was in an unmerged commit
on @herbelin's repo)
- commit message of 244d7a9aa contains a repro for its bug (I didn't
bother adding to the test suite as a return of the bug could just as
well use different strings so the specific repro wouldn't test
anything useful)
|
|
Ack-by: ggonthier
Reviewed-by: mattam82
|
|
Ack-by: gares
Ack-by: maximedenes
|
|
In particular evar_eqappr_x tries to find a miller pattern on both sides,
while the fast path for evars tries solve_simple_eqn in one direction
only. So if you have (Evar-not-miller = Evar-miller) the code was not
trying to solve the RHS.
|
|
Previously, they were hard-wired in the ML code.
|
|
Eliminators can be:
- dependent: ... -> forall x (y : I x), P x y
- truncated: ... -> forall x (y : I x), P x
- funind like: ..-> forall x, P t
The user may provide a term t in `elim: t`
- t may be the last argument
- t may be the last "pattern" (standing for the last
argument of P)
We use unification to see if t (and its type) fits
in one of these cases (and/or to infer t).
This patch refuses to use unification in the HO case
eg `?T a = t` since the result is too often a false
positive.
|
|
|
|
proj
Ack-by: gares
Reviewed-by: mattam82
Reviewed-by: maximedenes
|
|
applications
Reviewed-by: SkySkimmer
|
|
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jfehrle
|
|
This fixes an incompleteness of subtyping on cumulative inductives,
where I@{i} A <= I@{j} A should imply i <= j, i = j or no relation
depending on the variance of I's universe.
|
|
The `Coercion` command did report many ambiguous paths when one declared
multiple inheritances. This change makes the `Coercion` command to do not
report them when
1. all the coercion in the potentially ambiguous paths respect the uniform
inheritance condition and
2. functional compositions of the potentially ambiguous paths are convertible to
each other.
The first condition is not explicitly checked but is used to make the checking
process of the second condition easy.
The key idea of this change:
Let us consider a sequence of coercion
f_1 : C_1 >-> C_2, f_2 : C_2 >-> C_3, ..., f_n : C_n >-> C_(n+1)
which respect the uniform inheritance condition and where the user-defined
classes C_i have m_i parameters respectively (i <= n).
The functional composition f_1 . ... . f_n can be expressed as follows:
(fun x_1 ... x_(m_1) y =>
f_n _ ... _ (* m_n times repetition of holes *)
(...
(f_2 _ ... _ (* m_2 times repetition of holes *)
(f_1 x_1 ... x_(m_1) y))...)),
and the contents of all the holes can be determined (inferred) without leaving
any existential variables in them thanks to the uniform inheritance condition.
Misc:
- A test case for this change: test-suite/output/relaxed_ambiguous_paths.v
- Turn the ambiguous paths messages into warnings to do output test.
|
|
|
|
(NB: this needs relevance mark fixing)
|
|
Prevent errors when under annotating binders.
|
|
|
|
For nonsquashed:
Either
- 0 constructors
- primitive record
|
|
Kernel should be mostly correct, higher levels do random stuff at
times.
|
|
Note currently it's impossible to define inductives in SProp because
indtypes.ml and the pretyper aren't fully plugged.
|
|
|
|
Reviewed-by: gares
|
|
Ack-by: SkySkimmer
Reviewed-by: ejgallego
Ack-by: ppedrot
|
|
record
Reviewed-by: ejgallego
|
|
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: jashug
|
|
This causes the makefile to break due to dependencies when it fails,
and it's not worth adding a whole mess of code to catch the failure
for these files.
|
|
|
|
Reviewed-by: ejgallego
|
|
|
|
|
|
|
|
This is intended to be separate from handling of implicit binders.
The remaining uses of declare_manual_implicits satisfy a lot of
assertions, giving the possibility of simplifying the interface in the
future.
Two disabled warnings are added for things that currently pass silently.
Currently only Mtac passes non-maximal implicits to
declare_manual_implicits with the force-usage flag set. When implicit
arguments don't have to be named, should move Mtac over to
set_implicits.
|
|
|
|
|
|
|
|
|
|
|
|
Reviewed-by: SkySkimmer
|
|
Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
|
|
|
|
Reviewed-by: SkySkimmer
|
|
The `-boot` option was used to:
- suppress loading of the rc_file
- allow to save modules with prefix `Coq`
There is no good reason disable saving of modules with `Coq` prefix by
default, thus we remove this option.
Fixes: #9575
|
|
We may want to keep the make-based and Dune job, however the
make-based setup is tested by the INRIA workers so it may not be
needed.
In order for some test to run well, we always run in Dune with an
absolute path. The easiest way to get a portable absolute path is to
use OCaml itself so we introduce a small executable to do that.
While we are at it, we do some cleanup of the test-suite `dune` file,
in particular we remove useless comments, set `--no-buffer` so results
can be seen in real time, and recognize the `NJOBS` variable as we
have moved to a Dune version that supports env vars.
|
|
Reviewed-by: ejgallego
Ack-by: herbelin
Reviewed-by: mattam82
|
|
Parameters had to be removed in cases_pattern_of_glob_constr.
|
